Publications

Talks

  1. Higher Inductive Types, talk at FSCD/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. Constructing 1-truncated finitary higher inductive types as groupoid quotients, talk at HoTTEST2020
  12. Constructing Higher Inductive Types as Groupoid Quotients, talk at LICS2020
  13. Semantics for two-dimensional type theory, talk at Syntax and Semantics of Type Theories, Stockholm
  14. Semantics for two-dimensional type theory, talk at TYPES2022, Nantes

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. Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide
    Finite Sets in Homotopy Type Theory, CPP, pp. 201--214, ACM 2018.
    Webpage
  3. Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide
    Bicategories in Univalent Foundations, FSCD 2019, Vol. 131, pp. 5:1-5:17.
  4. Niccolò Veltri and Niels van der Weide
    Guarded Recursion in Agda via Sized Types, FSCD 2019, Vol. 131, pp. 31:1-32:19.
    Repository
  5. 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
  6. Niels van der Weide
    Constructing Higher Inductive Types as Groupoid Quotients, LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, July 2020, Pages 929–943.
  7. 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.
  8. Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, Niels van der Weide
    Bicategories in Univalent Foundations, Mathematical Structures in Computer Science, 1-38.
  9. Benedikt Ahrens, Paige Randall North, Niels van der Weide
    Semantics for two-dimensional type theory, LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, August 2022, Article 12, 1-14.

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

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