Abstract is missing.
- From Cubes to Twisted Cubes via Graph Morphisms in Type TheoryGun Pinyo, Nicolai Kraus. [doi]
- Type Theory Unchained: Extending Agda with User-Defined Rewrite RulesJesper Cockx. [doi]
- Is Impredicativity Implicitly Implicit?Stefan Monnier, Nathaniel Bos. [doi]
- A Quantitative Understanding of Pattern MatchingSandra Alves, Delia Kesner, Daniel Ventura. [doi]
- Coherence for Monoidal Groupoids in HoTTStefano Piceghello. [doi]
- Higher Inductive Type Eliminators Without PathsNils Anders Danielsson. [doi]
- Front Matter, Table of Contents, Preface, Conference Organization [doi]
- Making Isabelle Content Accessible in Knowledge Representation FormatsMichael Kohlhase, Florian Rabe, Makarius Wenzel. [doi]
- Big Step Normalisation for Type TheoryThorsten Altenkirch, Colin Geniet. [doi]
- For Finitary Induction-Induction, Induction Is EnoughAmbrus Kaposi, András Kovács, Ambroise Lafont. [doi]
- Eta-Equivalence in Core Dependent HaskellAnastasiya Kravchuk-Kirilyuk, Antoine Voizard, Stephanie Weirich. [doi]