TYPES 2016 May 23-26, 2016 - Novi Sad, Serbia

22nd International Conference on Types for Proofs and Programs (TYPES 2016)



Silvia Ghilezan and Herman Geuvers and Jelena Ivetić (Eds.)
ISBN 978-3-95977-065-1, LIPICS Vol. 97 ISSN 1868-8969
Additional Information
License
Conference Website
Complete volume (PDF, 7 MB)
Search Publication Server

Authors
  • Adams, Robin
  • Aschieri, Federico
  • Bauer, Andrej
  • Bezem, Marc
  • Booij, Auke B.
  • Chrzaszcz, Jacek
  • Coquand, Thierry
  • Czajka, Lukasz
  • Escardó, Martín H.
  • Espírito Santo, José
  • Frade, Maria João
  • Geuvers, Herman
  • Ghilezan, Silvia
  • Gilbert, Gaëtan
  • Harper, Robert
  • Haselwarter, Philipp G.
  • Hou (Favonia), Kuen-Bang
  • Igried, Bashar
  • Ivetic, Jelena
  • Lumsdaine, Peter LeFanu
  • Lungu, Georgiana Elena
  • Luo, Zhaohui
  • Manighetti, Matteo
  • Martin-Dorel, Érik
  • Miller, Dale
  • Nakata, Keiko
  • Parmann, Erik
  • Pinto, Luís
  • Pretnar, Matija
  • Ronchi Della Rocca, Simona
  • Schubert, Aleksy
  • Setzer, Anton
  • Shulman, Michael
  • Soloviev, Sergei
  • Statman, Richard
  • Stone, Christopher A.
  • Zakrzewski, Jakub
    		•

    		  
    Front Matter, Table of Contents, Preface, Conference Organization
    Authors: Ghilezan, Silvia ; Geuvers, Herman ; Ivetic, Jelena

    Abstract | Document (303 KB) | BibTeX

    Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper)
    Authors: Miller, Dale

    Abstract | Document (401 KB) | BibTeX

    Intersection Types and Denotational Semantics: An Extended Abstract (Invited Paper)
    Authors: Ronchi Della Rocca, Simona

    Abstract | Document (341 KB) | BibTeX

    A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic
    Authors: Adams, Robin ; Bezem, Marc ; Coquand, Thierry

    Abstract | Document (487 KB) | BibTeX

    On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic
    Authors: Aschieri, Federico ; Manighetti, Matteo

    Abstract | Document (587 KB) | BibTeX

    Design and Implementation of the Andromeda Proof Assistant
    Authors: Bauer, Andrej ; Gilbert, Gaëtan ; Haselwarter, Philipp G. ; Pretnar, Matija ; Stone, Christopher A.

    Abstract | Document (627 KB) | BibTeX

    Realizability at Work: Separating Two Constructive Notions of Finiteness
    Authors: Bezem, Marc ; Coquand, Thierry ; Nakata, Keiko ; Parmann, Erik

    Abstract | Document (520 KB) | BibTeX

    Parametricity, Automorphisms of the Universe, and Excluded Middle
    Authors: Booij, Auke B. ; Escardó, Martín H. ; Lumsdaine, Peter LeFanu ; Shulman, Michael

    Abstract | Document (453 KB) | BibTeX

    Coq Support in HAHA
    Authors: Chrzaszcz, Jacek ; Schubert, Aleksy ; Zakrzewski, Jakub

    Abstract | Document (746 KB) | BibTeX

    A Shallow Embedding of Pure Type Systems into First-Order Logic
    Authors: Czajka, Lukasz

    Abstract | Document (582 KB) | BibTeX

    Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts
    Authors: Espírito Santo, José ; Frade, Maria João ; Pinto, Luís

    Abstract | Document (616 KB) | BibTeX

    Covering Spaces in Homotopy Type Theory
    Authors: Hou (Favonia), Kuen-Bang ; Harper, Robert

    Abstract | Document (505 KB) | BibTeX

    Defining Trace Semantics for CSP-Agda
    Authors: Igried, Bashar ; Setzer, Anton

    Abstract | Document (683 KB) | BibTeX

    On Subtyping in Type Theories with Canonical Objects
    Authors: Lungu, Georgiana Elena ; Luo, Zhaohui

    Abstract | Document (653 KB) | BibTeX

    A Formal Study of Boolean Games with Random Formulas as Payoff Functions
    Authors: Martin-Dorel, Érik ; Soloviev, Sergei

    Abstract | Document (615 KB) | BibTeX

    The Completeness of BCD for an Operational Semantics
    Authors: Statman, Richard

    Abstract | Document (249 KB) | BibTeX

    		  



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