TYPES 2020 March 2-5, 2020, University of Turin, Italy

26th International Conference on Types for Proofs and Programs (TYPES 2020)



Ugo de'Liguoro and Stefano Berardi and Thorsten Altenkirch (Eds.)
ISBN 978-3-95977-182-5, LIPICS Vol. 188 ISSN 1868-8969
Additional Information
License
Conference Website
Complete volume (PDF, 4 MB)
Search Publication Server

Authors
  • Abel, Andreas
  • Affeldt, Reynald
  • Altenkirch, Thorsten
  • Berardi, Stefano
  • Blanqui, Frédéric
  • de'Liguoro, Ugo
  • De Luca, Guido
  • Espírito Santo, José
  • From, Asta Halkjær
  • Hondet, Gabriel
  • Honsell, Furio
  • Hugunin, Jasper
  • Lenisa, Marina
  • Luna, Carlos
  • Luo, Zhaohui
  • Maclean, Harry
  • Manighetti, Matteo
  • Matthes, Ralph
  • Miller, Dale
  • Momigliano, Alberto
  • Nowak, David
  • Pinto, Luís
  • Scagnetto, Ivan
  • Urzyczyn, Paweł
    		•

    		  
    Front Matter, Table of Contents, Preface, Conference Organization
    Authors: de'Liguoro, Ugo ; Berardi, Stefano ; Altenkirch, Thorsten

    Abstract | Document (469 KB) | BibTeX

    On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction
    Authors: Abel, Andreas

    Abstract | Document (872 KB) | BibTeX

    Extending Equational Monadic Reasoning with Monad Transformers
    Authors: Affeldt, Reynald ; Nowak, David

    Abstract | Document (893 KB) | BibTeX

    Towards a Certified Reference Monitor of the Android 10 Permission System
    Authors: De Luca, Guido ; Luna, Carlos

    Abstract | Document (783 KB) | BibTeX

    Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic
    Authors: Espírito Santo, José ; Matthes, Ralph ; Pinto, Luís

    Abstract | Document (879 KB) | BibTeX

    Synthetic Completeness for a Terminating Seligman-Style Tableau System
    Authors: From, Asta Halkjær

    Abstract | Document (817 KB) | BibTeX

    Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory
    Authors: Hondet, Gabriel ; Blanqui, Frédéric

    Abstract | Document (925 KB) | BibTeX

    Λ-Symsym: An Interactive Tool for Playing with Involutions and Types
    Authors: Honsell, Furio ; Lenisa, Marina ; Scagnetto, Ivan

    Abstract | Document (899 KB) | BibTeX

    Why Not W?
    Authors: Hugunin, Jasper

    Abstract | Document (656 KB) | BibTeX

    Subtype Universes
    Authors: Maclean, Harry ; Luo, Zhaohui

    Abstract | Document (776 KB) | BibTeX

    Two Applications of Logic Programming to Coq
    Authors: Manighetti, Matteo ; Miller, Dale ; Momigliano, Alberto

    Abstract | Document (819 KB) | BibTeX

    Duality in Intuitionistic Propositional Logic
    Authors: Urzyczyn, Paweł

    Abstract | Document (609 KB) | BibTeX

    		  



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