Abstract is missing.
- Front Matter, Table of Contents, Preface, Conference Organization [doi]
- Herbrand Disjunctions, Cut Elimination and Context-Free Tree GrammarsBahareh Afshari, Stefan Hetzl, Graham Emil Leigh. 1-16 [doi]
- Non-Wellfounded Trees in Homotopy Type TheoryBenedikt Ahrens, Paolo Capriotti, Régis Spadotti. 17-30 [doi]
- Conservativity of Embeddings in the lambda Pi Calculus Modulo RewritingAli Assaf. 31-44 [doi]
- Models for Polymorphism over Physical DimensionRobert Atkey, Neil Ghani, Fredrik Nordvall Forsberg, Timothy Revell, Sam Staton. 45-59 [doi]
- MALL Proof Equivalence is Logspace-Complete, via Binary Decision DiagramsMarc Bagnol. 60-75 [doi]
- Mixin Composition Synthesis Based on Intersection TypesJan Bessai, Andrej Dudenhefner, Boris Düdder, Tzu-Chun Chen, Ugo de'Liguoro, Jakob Rehof. 76-91 [doi]
- Non-Constructivity in Kan Simplicial SetsMarc Bezem, Thierry Coquand, Erik Parmann. 92-106 [doi]
- Logical Relations for Coherence of Effect SubtypingDariusz Biernacki, Piotr Polesiuk. 107-122 [doi]
- Observability for Pair Pattern CalculiAntonio Bucciarelli, Delia Kesner, Simona Ronchi Della Rocca. 123-137 [doi]
- Undecidability of Equality in the Free Locally Cartesian Closed CategorySimon Castellan, Pierre Clairambault, Peter Dybjer. 138-152 [doi]
- The Inconsistency of a Brouwerian Continuity Principle with the Curry-Howard InterpretationMartín Hötzel Escardó, Chuangjie Xu. 153-164 [doi]
- Curry-Howard for Sequent Calculus at Last!José Espírito Santo. 165-179 [doi]
- Dependent Types for Nominal Terms with Atom SubstitutionsElliot Fairweather, Maribel Fernández, Nora Szasz, Alvaro Tasistro. 180-195 [doi]
- Realizability Toposes from SpecificationsJonas Frey. 196-210 [doi]
- Standardization of a Call-By-Value Lambda-CalculusGiulio Guerrieri, Luca Paolini, Simona Ronchi Della Rocca. 211-225 [doi]
- Wild omega-Categories for the Homotopy Hypothesis in Type TheoryAndré Hirschowitz, Tom Hirschowitz, Nicolas Tabareau. 226-240 [doi]
- Multivariate Amortised Resource Analysis for Term Rewrite SystemsMartin Hofmann 0001, Georg Moser. 241-256 [doi]
- Termination of Dependently Typed Rewrite RulesJean-Pierre Jouannaud, Jianqi Li. 257-272 [doi]
- Well-Founded Recursion over Contextual ObjectsBrigitte Pientka, Andreas Abel 0001. 273-287 [doi]
- Polynomial Time in the Parametric Lambda CalculusBrian F. Redmond. 288-301 [doi]
- Fibrations of Tree AutomataColin Riba. 302-316 [doi]
- Multi-Focusing on Extensional Rewriting with SumsGabriel Scherer. 317-331 [doi]
- A Proof-theoretic Characterization of Independence in Type TheoryYuTing Wang, Kaustuv Chaudhuri. 332-346 [doi]