TYPES 2014 May 12-15, 2014 - Paris, France

20th International Conference on Types for Proofs and Programs (TYPES 2014)



Hugo Herbelin and Pierre Letouzey and Matthieu Sozeau (Eds.)
ISBN 978-3-939897-88-0, LIPICS Vol. 39 ISSN 1868-8969
Additional Information
License
Conference Website
Complete volume (PDF, 8 MB)
Search Publication Server

Authors
  • Ahrens, Benedikt
  • Assaf, Ali
  • Cauderlier, Raphaël
  • Danvy, Olivier
  • Dubois, Catherine
  • Hedges, Jules
  • Herbelin, Hugo
  • Keller, Chantal
  • Kraus, Nicolai
  • Krivine, Jean-Louis
  • Letouzey, Pierre
  • Maietti, Maria Emilia
  • Maschio, Samuele
  • Parmann, Erik
  • Pitts, Andrew M.
  • Polonsky, Andrew
  • Puech, Matthias
  • Schubert, Aleksy
  • Soloviev, Sergei
  • Sozeau, Matthieu
  • Spadotti, Régis
  • Steila, Silvia
  • Urzyczyn, Pawel
  • Walukiewicz-Chrzaszcz, Daria
    		•

    		  
    Front Matter, Table of Contents, Preface, Authors Index
    Authors: Herbelin, Hugo ; Letouzey, Pierre ; Sozeau, Matthieu

    Abstract | Document (317 KB) | BibTeX

    Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory
    Authors: Ahrens, Benedikt ; Spadotti, Régis

    Abstract | Document (585 KB) | BibTeX

    A Calculus of Constructions with Explicit Subtyping
    Authors: Assaf, Ali

    Abstract | Document (558 KB) | BibTeX

    Objects and Subtyping in the Lambda-Pi-Calculus Modulo
    Authors: Cauderlier, Raphaël ; Dubois, Catherine

    Abstract | Document (631 KB) | BibTeX

    Typeful Normalization by Evaluation
    Authors: Danvy, Olivier ; Keller, Chantal ; Puech, Matthias

    Abstract | Document (514 KB) | BibTeX

    Dialectica Categories and Games with Bidding
    Authors: Hedges, Jules

    Abstract | Document (500 KB) | BibTeX

    The General Universal Property of the Propositional Truncation
    Authors: Kraus, Nicolai

    Abstract | Document (687 KB) | BibTeX

    On the Structure of Classical Realizability Models of ZF
    Authors: Krivine, Jean-Louis

    Abstract | Document (545 KB) | BibTeX

    An Extensional Kleene Realizability Semantics for the Minimalist Foundation
    Authors: Maietti, Maria Emilia ; Maschio, Samuele

    Abstract | Document (652 KB) | BibTeX

    Investigating Streamless Sets
    Authors: Parmann, Erik

    Abstract | Document (484 KB) | BibTeX

    Nominal Presentation of Cubical Sets Models of Type Theory
    Authors: Pitts, Andrew M.

    Abstract | Document (538 KB) | BibTeX

    Extensionality of lambda-*
    Authors: Polonsky, Andrew

    Abstract | Document (625 KB) | BibTeX

    Restricted Positive Quantification Is Not Elementary
    Authors: Schubert, Aleksy ; Urzyczyn, Pawel ; Walukiewicz-Chrzaszcz, Daria

    Abstract | Document (635 KB) | BibTeX

    On Isomorphism of Dependent Products in a Typed Logical Framework
    Authors: Soloviev, Sergei

    Abstract | Document (500 KB) | BibTeX

    An Intuitionistic Analysis of Size-change Termination
    Authors: Steila, Silvia

    Abstract | Document (431 KB) | BibTeX

    		  



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