Abstract is missing.
- Expressing Ecumenical Systems in the λΠ-Calculus Modulo TheoryÉmilie Grienenberger. [doi]
- All Watched Over by Machines of Loving GraceDominic P. Mulligan. [doi]
- {mitten}: A Flexible Multimodal Proof AssistantPhilipp Stassen, Daniel Gratzer, Lars Birkedal. [doi]
- An Irrelevancy-Eliminating Translation of Pure Type SystemsNathan Mull. [doi]
- Classical Natural Deduction from Truth TablesHerman Geuvers, Tonny Hurkens. [doi]
- A Metatheoretic Analysis of Subtype UniversesFelix Bradley, Zhaohui Luo. [doi]
- Type Theory with Explicit Universe PolymorphismMarc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó. [doi]
- Linear Rank Intersection TypesFábio Reis, Sandra Alves, Mário Florido. [doi]
- The Münchhausen Method in Type TheoryThorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tamás Végh. [doi]
- A Univalent Formalization of Constructive Affine SchemesMax Zeuner, Anders Mörtberg. [doi]
- On the Fair Termination of Client-Server SessionsLuca Padovani. [doi]
- Univalent Monoidal CategoriesKobe Wullaert, Ralph Matthes, Benedikt Ahrens. [doi]
- Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term FamiliesCatherine Dubois, Nicolas Magaud, Alain Giorgetti. [doi]
- On Dynamic Lifting and Effect Typing in Circuit Description LanguagesAndrea Colledan, Ugo Dal Lago. [doi]
- Front Matter, Table of Contents, Preface, Conference Organization [doi]