Publications

You can also check dblp.

Conference Papers

  1. Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide
    Finite Sets in Homotopy Type Theory, CPP 2018, pp. 201-214.
    Webpage
  2. Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide
    Bicategories in Univalent Foundations, FSCD 2019, Vol. 131, pp. 5:1-5:17.
  3. Niccolò Veltri and Niels van der Weide
    Guarded Recursion in Agda via Sized Types, FSCD 2019, Vol. 131, pp. 31:1-32:19.
    Repository
  4. Niels van der Weide and Herman Geuvers
    The Construction of Set-Truncated Higher Inductive Types, MFPS 2019, Vol. 237 of ENTCS, pp. 261-280
  5. Niels van der Weide
    Constructing Higher Inductive Types as Groupoid Quotients, LICS 2020, pp. 929–943.
  6. Benedikt Ahrens, Paige Randall North, Niels van der Weide
    Semantics for two-dimensional type theory, LICS 2022, pp. 1-14.
  7. Niels van der Weide
    The Formal Theory of Monads, Univalently, FSCD 2023, Vol. 260, pp. 6:1-6:23.
  8. Niels van der Weide, Deivid Vale, Cynthia Kop
    Certifying Higher-Order Polynomial Interpretations, ITP 2023, Vol. 268, pp. 30:1-30:20.
  9. Niels van der Weide, Nima Rasekh, Benedikt Ahrens, Paige Randall North
    Univalent Double Categories, CPP 2024, pp. 246-259.
  10. Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert
    Displayed Monoidal Categories for the Semantics of Linear Logic, CPP 2024, pp. 260-273.
  11. 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.
  12. Niels van der Weide
    Univalent Enriched Categories and the Enriched Rezk Completion, FSCD 2024, Vol. 299, pp. 4:1-4:19.
  13. 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.
  14. Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, Niels van der Weide
    Intrinsically Correct Sorting in Cubical Agda, CPP 2025, pp. 34-49.
  15. Niels van der Weide
    The internal languages of univalent categories, LICS 2025, pp. 112-126.
  16. Steven Bronsveld, Herman Geuvers, Niels van der Weide
    Impredicative Encodings of Inductive and Coinductive Types, FSCD 2025, Vol. 337, pp. 11:1-11:22.
  17. 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
  18. 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.
  19. Kobe Wullaert, Niels van der Weide
    Rezk Completions of Elementary Topoi, accepted at TYPES postproceedings 2025.
  20. Sam Speight, Niels van der Weide
    Impredicativity in Linear Dependent Type Theory, under submission.

Journal Papers

  1. 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.
  2. 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.
  3. Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, Niels van der Weide
    Bicategories in Univalent Foundations, Mathematical Structures in Computer Science, 1-38.
  4. Benedikt Ahrens, Paige Randall North, Niels van der Weide
    Bicategorical type theory: semantics and syntax, Mathematical Structures in Computer Science, 1-45.
  5. 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.
  6. Niels van der Weide
    Univalent Enriched Categories and the Enriched Rezk Completion, accepted at Logical Methods in Computer Science.
  7. Niels van der Weide
    The internal languages of univalent categories, under submission.

Extended Abstracts

  1. Dan Frumin, Herman Geuvers, Niels van der Weide
    1-Types vs Groupoids, TYPES 2018, Braga
  2. Henning Basold, Niccolò Veltri, Niels van der Weide
    Free Algebraic Theories as Higher Inductive Types, TYPES 2019, Oslo
  3. Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide
    Bicategories in Univalent Foundations, TYPES 2019, Oslo
  4. Niccolò Veltri, Niels van der Weide
    Guarded Recursion in Agda via Sized Types, TYPES 2019, Oslo
  5. Niels van der Weide
    Constructing Higher Inductive Types as Groupoid Quotients, TYPES 2020
  6. Deivid Vale, Niels van der Weide
    Formalizing Higher-Order Termination in Coq, WST 2021
  7. Benedikt Ahrens, Paige Randall North, Niels van der Weide
    Semantics for two-dimensional type theory, TYPES 2022, Nantes
  8. Benedikt Ahrens, Paige Randall North, Niels van der Weide
    Semantics for two-dimensional type theory, HoTT/UF 2022, Haifa
  9. Niels van der Weide
    Enriched Categories in Univalent Foundations, HoTT/UF 2023, Vienna
  10. Niels van der Weide
    Enriched Categories in Univalent Foundations, TYPES 2023, Valencia
  11. Niels van der Weide and Kobe Wullaert
    Rezk Completion of Bicategories, TYPES 2023, Valencia
  12. Cynthia Kop, Deivid Vale and Niels van der Weide
    Nijn/ONijn: A New Certification Engine for Higher-Order Termination, HOR 2023, Rome
  13. Nima Rasekh, Niels van der Weide, Benedikt Ahrens, Paige Randall North
    The Univalence Maxim and Univalent Double Categories, TYPES 2024, Copenhagen
  14. Niels van der Weide
    The Internal Language of Univalent Categories, TYPES 2024, Copenhagen
  15. Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens, Paige Randall North
    A Type Theory for Comprehension Categories with Applications to Subtyping, TYPES 2025, Glasgow
  16. Herman Geuvers, Niels van der Weide, Steven Bronsveld
    Impredicative Encodings of Inductive and Coinductive Types, TYPES 2025, Glasgow
  17. Kobe Wullaert, Niels van der Weide
    Rezk completions For (Elementary) Topoi, TYPES 2025, Glasgow
  18. Niyousha Najmaei Wullaert, Niels van der Weide
    A General Construction of Strict Models in HoTT, TYPES 2026, Gothenburg
  19. Sam Speight, Niels van der Weide
    Impredicative Encodings of Linear Types, TYPES 2026, Gothenburg
  20. Sam Speight, Niels van der Weide
    Internal Models of Linear Type Theories

Theses

  1. Computing Exact Solutions of Initial Value Problems, Bachelor Thesis Computer Science
  2. Model Structures on Toposes, Master Thesis Mathematics
  3. Higher Inductive Types, Master Thesis Computer Science
  4. Constructing Higher Inductive Types, PhD Thesis Computer Science