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 Theoy 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

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, Accepted at FSCD 2019.
  4. Niccolò Veltri and Niels van der Weide
    Guarded Recursion in Agda via Sized Types, Accepted at FSCD 2019.
    Repository
  5. Niels van der Weide and Herman Geuvers
    The Construction of Set-Truncated Higher Inductive Types, Accepted at MFPS 2019
    Repository

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

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

Informal Talks

  1. Programming with Higher Inductive Types, talk at Brouwer Seminar.
  2. Inductive Predicates, talk at CPDT reading group.