LIPIcs, Volume 239, TYPES 2021

• Henning Basold, Jesper Cockx, and Silvia Ghilezan LIPIcs, Volume 239, TYPES 2021, Complete Volume 10.4230/LIPIcs.TYPES.2021
• Henning Basold, Jesper Cockx, and Silvia Ghilezan Front Matter, Table of Contents, Preface, Conference Organization 10.4230/LIPIcs.TYPES.2021.0
• Fahad F. Alhabardi, Arnold Beckmann, Bogdan Lazar, and Anton Setzer Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control 10.4230/LIPIcs.TYPES.2021.1
• Thibaut Benjamin Formalisation of Dependent Type Theory: The Example of CaTT 10.4230/LIPIcs.TYPES.2021.2
• Rafaël Bocquet Strictification of Weakly Stable Type-Theoretic Structures Using Generic Contexts 10.4230/LIPIcs.TYPES.2021.3
• William DeMeo and Jacques Carette A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-Löf Type Theory 10.4230/LIPIcs.TYPES.2021.4
• Pietro Di Gianantonio and Marina Lenisa Principal Types as Lambda Nets 10.4230/LIPIcs.TYPES.2021.5
• István Donkó and Ambrus Kaposi Internal Strict Propositions Using Point-Free Equations 10.4230/LIPIcs.TYPES.2021.6
• Giulio Fellin, Sara Negri, and Eugenio Orlandelli Constructive Cut Elimination in Geometric Logic 10.4230/LIPIcs.TYPES.2021.7
• Asta Halkjær From A Succinct Formalization of the Completeness of First-Order Logic 10.4230/LIPIcs.TYPES.2021.8
• Christa Jenkins, Andrew Marmaduke, and Aaron Stump Simulating Large Eliminations in Cedille 10.4230/LIPIcs.TYPES.2021.9
• Georgi Nakov and Fredrik Nordvall Forsberg Quantitative Polynomial Functors 10.4230/LIPIcs.TYPES.2021.10
• Joseph W. N. Paulus, Daniele Nantes-Sobrinho, and Jorge A. Pérez Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes 10.4230/LIPIcs.TYPES.2021.11
• Yuta Takahashi Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus 10.4230/LIPIcs.TYPES.2021.12