TYPES 2021 June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)

27th International Conference on Types for Proofs and Programs (TYPES 2021)



Henning Basold and Jesper Cockx and Silvia Ghilezan (Eds.)
ISBN 978-3-95977-254-9, LIPICS Vol. 239 ISSN 1868-8969
Additional Information
License
Conference Website
Complete volume (PDF, 4 MB)
Search Publication Server

Authors
  • Alhabardi, Fahad F.
  • Basold, Henning
  • Beckmann, Arnold
  • Benjamin, Thibaut
  • Bocquet, Rafaël
  • Carette, Jacques
  • Cockx, Jesper
  • DeMeo, William
  • Di Gianantonio, Pietro
  • Donkó, István
  • Fellin, Giulio
  • From, Asta Halkjær
  • Ghilezan, Silvia
  • Jenkins, Christa
  • Kaposi, Ambrus
  • Lazar, Bogdan
  • Lenisa, Marina
  • Marmaduke, Andrew
  • Nakov, Georgi
  • Nantes-Sobrinho, Daniele
  • Negri, Sara
  • Nordvall Forsberg, Fredrik
  • Orlandelli, Eugenio
  • Paulus, Joseph W. N.
  • Pérez, Jorge A.
  • Setzer, Anton
  • Stump, Aaron
  • Takahashi, Yuta
    		•

    		  
    Front Matter, Table of Contents, Preface, Conference Organization
    Authors: Basold, Henning ; Cockx, Jesper ; Ghilezan, Silvia

    Abstract | Document (479 KB) | BibTeX

    Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control
    Authors: Alhabardi, Fahad F. ; Beckmann, Arnold ; Lazar, Bogdan ; Setzer, Anton

    Abstract | Document (830 KB) | BibTeX

    Formalisation of Dependent Type Theory: The Example of CaTT
    Authors: Benjamin, Thibaut

    Abstract | Document (853 KB) | BibTeX

    Strictification of Weakly Stable Type-Theoretic Structures Using Generic Contexts
    Authors: Bocquet, Rafaël

    Abstract | Document (508 KB) | BibTeX

    A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-Löf Type Theory
    Authors: DeMeo, William ; Carette, Jacques

    Abstract | Document (464 KB) | BibTeX

    Principal Types as Lambda Nets
    Authors: Di Gianantonio, Pietro ; Lenisa, Marina

    Abstract | Document (853 KB) | BibTeX

    Internal Strict Propositions Using Point-Free Equations
    Authors: Donkó, István ; Kaposi, Ambrus

    Abstract | Document (769 KB) | BibTeX

    Constructive Cut Elimination in Geometric Logic
    Authors: Fellin, Giulio ; Negri, Sara ; Orlandelli, Eugenio

    Abstract | Document (825 KB) | BibTeX

    A Succinct Formalization of the Completeness of First-Order Logic
    Authors: From, Asta Halkjær

    Abstract | Document (773 KB) | BibTeX

    Simulating Large Eliminations in Cedille
    Authors: Jenkins, Christa ; Marmaduke, Andrew ; Stump, Aaron

    Abstract | Document (832 KB) | BibTeX

    Quantitative Polynomial Functors
    Authors: Nakov, Georgi ; Nordvall Forsberg, Fredrik

    Abstract | Document (886 KB) | BibTeX

    Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes
    Authors: Paulus, Joseph W. N. ; Nantes-Sobrinho, Daniele ; Pérez, Jorge A.

    Abstract | Document (1,013 KB) | BibTeX

    Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus
    Authors: Takahashi, Yuta

    Abstract | Document (937 KB) | BibTeX

    		  



    DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI