Abstract is missing.
- Design and Implementation of the Andromeda Proof AssistantAndrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, Christopher A. Stone. [doi]
- A Formal Study of Boolean Games with Random Formulas as Payoff FunctionsÉrik Martin-Dorel, Sergei Soloviev. [doi]
- Permutability in Proof Terms for Intuitionistic Sequent Calculus with CutsJosé Espírito Santo, Maria João Frade, Luís Pinto. [doi]
- Realizability at Work: Separating Two Constructive Notions of FinitenessMarc Bezem, Thierry Coquand, Keiko Nakata 0001, Erik Parmann. [doi]
- Parametricity, Automorphisms of the Universe, and Excluded MiddleAuke Bart Booij, Martín Hötzel Escardó, Peter LeFanu Lumsdaine, Michael Shulman. [doi]
- A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal LogicRobin Adams, Marc Bezem, Thierry Coquand. [doi]
- Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper)Dale Miller 0001. [doi]
- Coq Support in HAHAJacek Chrzaszcz, Aleksy Schubert, Jakub Zakrzewski 0001. [doi]
- On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and ArithmeticFederico Aschieri, Matteo Manighetti. [doi]
- Covering Spaces in Homotopy Type TheoryKuen-Bang Hou (Favonia), Robert Harper 0001. [doi]
- On Subtyping in Type Theories with Canonical ObjectsGeorgiana E. Lungu, Zhaohui Luo. [doi]
- Intersection Types and Denotational Semantics: An Extended Abstract (Invited Paper)Simona Ronchi Della Rocca. [doi]
- The Completeness of BCD for an Operational SemanticsRichard Statman. [doi]
- A Shallow Embedding of Pure Type Systems into First-Order LogicLukasz Czajka 0001. [doi]
- Defining Trace Semantics for CSP-AgdaBashar Igried, Anton Setzer. [doi]
- Front Matter, Table of Contents, Preface, Conference Organization [doi]