Publications
☰
You can also check
dblp .
Conference Papers
Kobe Wullaert, Niels van der Weide
Rezk Completions of Elementary Topoi , accepted at TYPES postproceedings 2025.
Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens, Paige Randall North
From Semantics to Syntax: A Type Theory for Comprehension Categories , POPL 2026, PACMPL Volume 10, pp. 2409-2438.
Simcha van Collem, Niels van der Weide and Herman Geuvers
Initial Algebras of Domains via Quotient Inductive-Inductive Types , MFPS 2025, Vol. 5 of ENTCS
Steven Bronsveld, Herman Geuvers, Niels van der Weide
Impredicative Encodings of Inductive and Coinductive Types , FSCD 2025, Vol. 337, pp. 11:1-11:22.
Niels van der Weide
The internal languages of univalent categories , LICS 2025, pp. 112-126.
Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, Niels van der Weide
Intrinsically Correct Sorting in Cubical Agda , CPP 2025, pp. 34-49.
Nima Rasekh, Niels van der Weide, Benedikt Ahrens, Paige Randall North
Insights From Univalent Foundations: A Case Study Using Double Categories , CSL 2025, Vol. 326, pp. 45:1-45:18.
Niels van der Weide
Univalent Enriched Categories and the Enriched Rezk Completion , FSCD 2024, Vol. 299, pp. 4:1-4:19.
Niels van der Weide and Dan Frumin
The Interval Domain in Homotopy Type Theory , Geuversfest60, Logics and Type Systems in Theory and Practice. Lecture Notes in Computer Science, vol 14560.
Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert
Displayed Monoidal Categories for the Semantics of Linear Logic , CPP 2024, pp. 260-273.
Niels van der Weide, Nima Rasekh, Benedikt Ahrens, Paige Randall North
Univalent Double Categories , CPP 2024, pp. 246-259.
Niels van der Weide, Deivid Vale, Cynthia Kop
Certifying Higher-Order Polynomial Interpretations , ITP 2023, Vol. 268, pp. 30:1-30:20.
Niels van der Weide
The Formal Theory of Monads, Univalently , FSCD 2023, Vol. 260, pp. 6:1-6:23.
Benedikt Ahrens, Paige Randall North, Niels van der Weide
Semantics for two-dimensional type theory , LICS 2022, pp. 1-14.
Niels van der Weide
Constructing Higher Inductive Types as Groupoid Quotients , LICS 2020, pp. 929–943.
Niels van der Weide and Herman Geuvers
The Construction of Set-Truncated Higher Inductive Types , MFPS 2019, Vol. 237 of ENTCS, pp. 261-280
Niccolò Veltri and Niels van der Weide
Guarded Recursion in Agda via Sized Types , FSCD 2019, Vol. 131, pp. 31:1-32:19.
Repository
Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide
Bicategories in Univalent Foundations , FSCD 2019, Vol. 131, pp. 5:1-5:17.
Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide
Finite Sets in Homotopy Type Theory , CPP 2018, pp. 201-214.
Webpage
Journal Papers
Niels van der Weide
Univalent Enriched Categories and the Enriched Rezk Completion , Logical Methods in Computer Science , Volume 22, Issue 2, 2026, pp. 25:1-25:29 (invited for special issue of FSCD 2024).
Niels van der Weide
The Formal Theory of Monads, Univalently , Logical Methods in Computer Science , Volume 21, Issue 1, 2025, pp. 16:1–16:30 (invited for special issue of FSCD 2023).
Benedikt Ahrens, Paige Randall North, Niels van der Weide
Bicategorical type theory: semantics and syntax , Mathematical Structures in Computer Science , 1-45.
Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, Niels van der Weide
Bicategories in Univalent Foundations , Mathematical Structures in Computer Science , 1-38.
Niccolò Veltri and Niels van der Weide
Constructing Higher Inductive Types as Groupoid Quotients , Logical Methods in Computer Science , Volume 17, Issue 2, 2021, pp. 8:1–8:42.
Henning Basold, Herman Geuvers, Niels van der Weide
Higher Inductive Types in Programming , Journal of Universal Computer Science , Vol. 23, No. 1, pp. 63-88.
Preprints
Sam Speight, Niels van der Weide
Impredicativity in Linear Dependent Type Theory , under submission.
Niels van der Weide
The internal languages of univalent categories (extended version), under submission.
Extended Abstracts
Sam Speight, Niels van der Weide
Internal Models of Linear Type Theories , TLLA , 2026, Lisbon
Sam Speight, Niels van der Weide
Impredicative Encodings of Linear Types , TYPES 2026, Gothenburg
Niyousha Najmaei Wullaert, Niels van der Weide
A General Construction of Strict Models in HoTT , TYPES 2026, Gothenburg
Kobe Wullaert, Niels van der Weide
Rezk completions For (Elementary) Topoi , TYPES 2025, Glasgow
Herman Geuvers, Niels van der Weide, Steven Bronsveld
Impredicative Encodings of Inductive and Coinductive Types , TYPES 2025, Glasgow
Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens, Paige Randall North
A Type Theory for Comprehension Categories with Applications to Subtyping , TYPES 2025, Glasgow
Niels van der Weide
The Internal Language of Univalent Categories , TYPES 2024, Copenhagen
Nima Rasekh, Niels van der Weide, Benedikt Ahrens, Paige Randall North
The Univalence Maxim and Univalent Double Categories , TYPES 2024, Copenhagen
Cynthia Kop, Deivid Vale and Niels van der Weide
Nijn/ONijn: A New Certification Engine for Higher-Order Termination , HOR 2023, Rome
Niels van der Weide and Kobe Wullaert
Rezk Completion of Bicategories , TYPES 2023, Valencia
Niels van der Weide
Enriched Categories in Univalent Foundations , TYPES 2023, Valencia
Niels van der Weide
Enriched Categories in Univalent Foundations , HoTT/UF 2023, Vienna
Benedikt Ahrens, Paige Randall North, Niels van der Weide
Semantics for two-dimensional type theory , HoTT/UF 2022, Haifa
Benedikt Ahrens, Paige Randall North, Niels van der Weide
Semantics for two-dimensional type theory , TYPES 2022, Nantes
Deivid Vale, Niels van der Weide
Formalizing Higher-Order Termination in Coq , WST 2021
Niels van der Weide
Constructing Higher Inductive Types as Groupoid Quotients , TYPES 2020
Niccolò Veltri, Niels van der Weide
Guarded Recursion in Agda via Sized Types , TYPES 2019, Oslo
Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide
Bicategories in Univalent Foundations , TYPES 2019, Oslo
Henning Basold, Niccolò Veltri, Niels van der Weide
Free Algebraic Theories as Higher Inductive Types , TYPES 2019, Oslo
Dan Frumin, Herman Geuvers, Niels van der Weide
1-Types vs Groupoids , TYPES 2018, Braga
Theses
Computing Exact Solutions of Initial Value Problems , Bachelor Thesis Computer Science
Model Structures on Toposes , Master Thesis Mathematics
Higher Inductive Types , Master Thesis Computer Science
Constructing Higher Inductive Types , PhD Thesis Computer Science