Publications

Conference Papers

  1. Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide
    Finite Sets in Homotopy Type Theory, CPP, pp. 201-214, ACM 2018.
    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 ENTC, pp. 261-280
    Repository
  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, CPP2024, pp. 246-259.
  10. Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert
    Displayed Monoidal Categories for the Semantics of Linear Logic, CPP2024, pp. 260-273.
  11. Niels van der Weide
    Univalent Enriched Categories and the Enriched Rezk Completion, accepted.
  12. Nima Rasekh, Niels van der Weide, Benedikt Ahrens, Paige Randall North
    Insights From Univalent Foundations: A Case Study Using Double Categories, submitted.

Journal Papers

  1. Henning Basold, Herman Geuvers, Niels van der Weide
    Programming with Higher Inductive Types, 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, submitted.

Talks

  1. Higher Inductive Types, talk at HoTT/UF 2016, Porto.
  2. Programming with Higher Inductive Types, talk at EUTYPES meeting, Ljubljana.
  3. The Three-HITs Theorem, talk at FPFM workshop, Nantes.
  4. Higher Inductive Types in Programming, talk at Agda Implementors Meeting XXV, Gothenburg.
  5. Finite Sets in HoTT, talk at EUTYPES meeting in Nijmegen.
  6. 1-Types vs Groupoids, talk at TYPES2018, Braga.
  7. Bicategories in Homotopy Type Theory, talk at EUTYPES meeting in Aarhus.
  8. Category Theory in UniMath, talk at UniMath School II 2019, Birmingham.
  9. Bicategories in Univalent Foundations, talk at TYPES2019, Oslo.
  10. Bicategories in Univalent Foundations, talk at FSCD2019, Dortmund.
  11. The Construction of Set-Truncated Higher Inductive Types, talk at MFPS. London.
  12. Constructing 1-truncated finitary higher inductive types as groupoid quotients, talk at HoTTEST2020.
  13. Constructing Higher Inductive Types as Groupoid Quotients, talk at LICS2020.
  14. Semantics for two-dimensional type theory, talk at Syntax and Semantics of Type Theories, Stockholm.
  15. Semantics for two-dimensional type theory, talk at TYPES2022, Nantes.
  16. Category Theory in UniMath, talk at UniMath School III 2022, Cortona, Italy.
  17. Enriched Categories in Univalent Foundations, talk at HoTT/UF 2023, Vienna, Austria.
  18. Enriched Categories in Univalent Foundations, talk at TYPES 2023, Valencia, Spain.
  19. The Formal Theory of Monads, Univalently, talk at FSCD 2023, Rome, Italy.
  20. Displayed Monoidal Categories for the Semantics of Linear Logic, talk at CPP 2024, London, UK.
  21. Displayed Monoidal Categories for the Semantics of Linear Logic, talk at SWS seminar.
  22. Certifying higher-order polynomial interpretations, talk at rewritig/logic seminar.
  23. The Internal Language of Univalent Categories, talk at the Programming Languages Seminar in Delft.
  24. Formalizing Double Categories in UniMath, talk at the CoREACT Seminar.

Extended Abstracts

  1. Dan Frumin, Herman Geuvers, Niels van der Weide
    1-Types vs Groupoids, TYPES2018, Braga
  2. Henning Basold, Niccolò Veltri, Niels van der Weide
    Free Algebraic Theories as Higher Inductive Types, TYPES2019, Oslo
  3. Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide
    Bicategories in Univalent Foundations, TYPES2019, Oslo
  4. Niccolò Veltri, Niels van der Weide
    Guarded Recursion in Agda via Sized Types, TYPES2019, Oslo
  5. Niels van der Weide
    Constructing Higher Inductive Types as Groupoid Quotients, TYPES2020
  6. Deivid Vale, Niels van der Weide
    Formalizing Higher-Order Termination in Coq, WST2021
  7. Benedikt Ahrens, Paige Randall North, Niels van der Weide
    Semantics for two-dimensional type theory, TYPES2022, Nantes
  8. Benedikt Ahrens, Paige Randall North, Niels van der Weide
    Semantics for two-dimensional type theory, HoTT/UF2022, Haifa
  9. Niels van der Weide
    Enriched Categories in Univalent Foundations, HoTT/UF2023, Vienna
  10. Niels van der Weide
    Enriched Categories in Univalent Foundations, Types 2023, Valencia

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