Abstract is missing.
- Frontmatter, Table of Contents, Preface, Conference Organization [doi]
- Update Monads: Cointerpreting Directed ContainersDanel Ahman, Tarmo Uustalu. 1-23 [doi]
- A "Game Semantical" Intuitionistic Realizability Validating Markov's PrincipleFederico Aschieri, Margherita Zorzi. 24-44 [doi]
- Formally Verified Implementation of an Idealized Model of VirtualizationGilles Barthe, Gustavo Betarte, Juan Diego Campo, Jesús Mauricio Chimento, Carlos Luna. 45-63 [doi]
- Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic ArithmeticStefano Berardi, Silvia Steila. 64-83 [doi]
- Extracting Imperative Programs from Proofs: In-place QuicksortUlrich Berger, Monika Seisenberger, Gregory J. M. Woods. 84-106 [doi]
- A Model of Type Theory in Cubical SetsMarc Bezem, Thierry Coquand, Simon Huber. 107-128 [doi]
- Isomorphism of "Functional" Intersection TypesMario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria, Maddalena Zacchi. 129-149 [doi]
- A Hybrid Linear Logic for Constrained Transition SystemsJoëlle Despeyroux, Kaustuv Chaudhuri. 150-168 [doi]
- The Rooster and the Syntactic BracketHugo Herbelin, Arnaud Spiwack. 169-187 [doi]
- A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control OperatorsDanko Ilik, Keiko Nakata. 188-201 [doi]
- The Montagovian Generative Lexicon Lambda Ty_n: a Type Theoretical Framework for Natural Language SemanticsChristian Retoré. 202-229 [doi]
- A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative LanguageLeonardo Rodríguez, Daniel Fridlender, Miguel Pagano. 230-250 [doi]
- Definitional Extension in Type TheoryTao Xue. 251-269 [doi]