| 157 | -- | 158 | Peter LeFanu Lumsdaine, Nicolas Tabareau. Preface: Special Issue on Homotopy Type Theory and Univalent Foundations |
| 159 | -- | 171 | Marc Bezem, Thierry Coquand, Simon Huber. The Univalence Axiom in Cubical Sets |
| 173 | -- | 210 | Simon Huber. Canonicity for Cubical Type Theory |
| 211 | -- | 253 | Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi. Guarded Cubical Type Theory |
| 255 | -- | 284 | Guillaume Brunerie. 3) in Homotopy Type Theory |
| 285 | -- | 318 | Benedikt Ahrens, Ralph Matthes, Anders Mörtberg. From Signatures to Monads in UniMath |
| 319 | -- | 321 | Mauricio Ayala-Rincón, César A. Muñoz. Selected Extended Papers of ITP 2017 - Preface |
| 323 | -- | 345 | Xavier Allamigeon, Ricardo D. Katz. A Formalization of Convex Polyhedra Based on the Simplex Method |
| 347 | -- | 368 | Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow. A Formal Proof of the Expressiveness of Deep Learning |
| 369 | -- | 392 | Frédéric Besson, Sandrine Blazy, Pierre Wilke. CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics |
| 393 | -- | 413 | Yannick Forster 0002, Gert Smolka. Call-by-Value Lambda Calculus as a Model of Computation in Coq |
| 415 | -- | 438 | Dominik Kirst, Gert Smolka. Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory |
| 439 | -- | 462 | Andreas Lochbihler. Effect Polymorphism in Higher-Order Logic (Proof Pearl) |
| 463 | -- | 488 | Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola. A Verified Generational Garbage Collector for CakeML |
| 489 | -- | 515 | Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek. Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology |
| 517 | -- | 538 | Bohua Zhan. Formalization of the Fundamental Group in Untyped Set Theory Using Auto2 |