Abstract is missing.
- Types and Terms Translated: Unrestricted Resources in Encoding Functions as ProcessesJoseph W. N. Paulus, Daniele Nantes Sobrinho, Jorge A. Pérez 0001. [doi]
- Strictification of Weakly Stable Type-Theoretic Structures Using Generic ContextsRafaël Bocquet. [doi]
- Formalisation of Dependent Type Theory: The Example of CaTTThibaut Benjamin. [doi]
- Constructive Cut Elimination in Geometric LogicGiulio Fellin, Sara Negri, Eugenio Orlandelli. [doi]
- Front Matter, Table of Contents, Preface, Conference Organization [doi]
- Size-Based Termination for Non-Positive Types in Simply Typed Lambda-CalculusYuta Takahashi. [doi]
- Quantitative Polynomial FunctorsGeorgi Nakov, Fredrik Nordvall Forsberg. [doi]
- A Succinct Formalization of the Completeness of First-Order LogicAsta Halkjær From. [doi]
- A Machine-Checked Proof of Birkhoff's Variety Theorem in Martin-Löf Type TheoryWilliam J. DeMeo, Jacques Carette. [doi]
- Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access ControlFahad F. Alhabardi, Arnold Beckmann, Bogdan Lazar, Anton Setzer. [doi]
- Simulating Large Eliminations in CedilleChrista Jenkins, Andrew Marmaduke, Aaron Stump. [doi]
- Internal Strict Propositions Using Point-Free EquationsIstván Donkó, Ambrus Kaposi. [doi]
- Principal Types as Lambda NetsPietro Di Gianantonio, Marina Lenisa. [doi]