Publications
Talks
- Higher Inductive Types, talk at FSCD/UF 2016, Porto.
- Programming with Higher Inductive Types, talk at EUTYPES meeting, Ljubljana.
- The Three-HITs Theorem, talk at FPFM workshop, Nantes.
- Higher Inductive Types in Programming, talk at Agda Implementors Meeting XXV, Gothenburg.
- Finite Sets in HoTT, talk at EUTYPES meeting in Nijmegen
- 1-Types vs Groupoids, talk at TYPES2018, Braga
- Bicategories in Homotopy Type Theory, talk at EUTYPES meeting in Aarhus
- Category Theoy in UniMath, talk at UniMath School II 2019, Birmingham
- Bicategories in Univalent Foundations, talk at TYPES2019, Oslo
- Bicategories in Univalent Foundations, talk at FSCD2019, Dortmund
Papers
- 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.
- Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide
Finite Sets in Homotopy Type Theory, CPP, pp. 201--214, ACM 2018.
Webpage
- Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide
Bicategories in Univalent Foundations, Accepted at FSCD 2019.
- Niccolò Veltri and Niels van der Weide
Guarded Recursion in Agda via Sized Types, Accepted at FSCD 2019.
Repository
- Niels van der Weide and Herman Geuvers
The Construction of Set-Truncated Higher Inductive Types, Accepted at MFPS 2019
Repository
Extended Abstracts
- Dan Frumin, Herman Geuvers, Niels van der Weide
1-Types vs Groupoids, TYPES2018, Braga
- Henning Basold, Niccolò Veltri, Niels van der Weide
Free Algebraic Theories as Higher Inductive Types, TYPES2019, Oslo
- Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide
Bicategories in Univalent Foundations, TYPES2019, Oslo
- Niccolò Veltri, Niels van der Weide
Guarded Recursion in Agda via Sized Types, TYPES2019, Oslo
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
Informal Talks
- Programming with Higher Inductive Types, talk at Brouwer Seminar.
- Inductive Predicates, talk at CPDT reading group.