TYPES 2013 April 22-26, 2013 - Toulouse, France

19th International Conference on Types for Proofs and Programs (TYPES 2013)



Ralph Matthes and Aleksy Schubert (Eds.)
ISBN 978-3-939897-72-9, LIPICS Vol. 26 ISSN 1868-8969
Additional Information
License
Conference Website
Complete volume (PDF, 9 MB)
Search Publication Server

Authors
  • Ahman, Danel
  • Aschieri, Federico
  • Barthe, Gilles
  • Berardi, Stefano
  • Berger, Ulrich
  • Betarte, Gustavo
  • Bezem, Marc
  • Campo, Juan Diego
  • Chaudhuri, Kaustuv
  • Chimento, Jesús Mauricio
  • Coppo, Mario
  • Coquand, Thierry
  • Despeyroux, Joëlle
  • Dezani-Ciancaglini, Mariangiola
  • Fridlender, Daniel
  • Herbelin, Hugo
  • Huber, Simon
  • Ilik, Danko
  • Luna, Carlos
  • Margaria, Ines
  • Matthes, Ralph
  • Nakata, Keiko
  • Pagano, Miguel
  • Retoré, Christian
  • Rodríguez, Leonardo
  • Schubert, Aleksy
  • Seisenberger, Monika
  • Spiwack, Arnaud
  • Steila, Silvia
  • Uustalu, Tarmo
  • Woods, Gregory J. M.
  • Xue, Tao
  • Zacchi, Maddalena
  • Zorzi, Margherita
    		•

    		  
    Frontmatter, Table of Contents, Preface, Conference Organization
    Authors: Matthes, Ralph ; Schubert, Aleksy

    Abstract | Document (301 KB) | BibTeX

    Update Monads: Cointerpreting Directed Containers
    Authors: Ahman, Danel ; Uustalu, Tarmo

    Abstract | Document (537 KB) | BibTeX

    A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle
    Authors: Aschieri, Federico ; Zorzi, Margherita

    Abstract | Document (632 KB) | BibTeX

    Formally Verified Implementation of an Idealized Model of Virtualization
    Authors: Barthe, Gilles ; Betarte, Gustavo ; Campo, Juan Diego ; Chimento, Jesús Mauricio ; Luna, Carlos

    Abstract | Document (540 KB) | BibTeX

    Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic
    Authors: Berardi, Stefano ; Steila, Silvia

    Abstract | Document (510 KB) | BibTeX

    Extracting Imperative Programs from Proofs: In-place Quicksort
    Authors: Berger, Ulrich ; Seisenberger, Monika ; Woods, Gregory J. M.

    Abstract | Document (555 KB) | BibTeX

    A Model of Type Theory in Cubical Sets
    Authors: Bezem, Marc ; Coquand, Thierry ; Huber, Simon

    Abstract | Document (588 KB) | BibTeX

    Isomorphism of "Functional" Intersection Types
    Authors: Coppo, Mario ; Dezani-Ciancaglini, Mariangiola ; Margaria, Ines ; Zacchi, Maddalena

    Abstract | Document (645 KB) | BibTeX

    A Hybrid Linear Logic for Constrained Transition Systems
    Authors: Despeyroux, Joëlle ; Chaudhuri, Kaustuv

    Abstract | Document (663 KB) | BibTeX

    The Rooster and the Syntactic Bracket
    Authors: Herbelin, Hugo ; Spiwack, Arnaud

    Abstract | Document (459 KB) | BibTeX

    A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators
    Authors: Ilik, Danko ; Nakata, Keiko

    Abstract | Document (567 KB) | BibTeX

    The Montagovian Generative Lexicon Lambda Ty_n: a Type Theoretical Framework for Natural Language Semantics
    Authors: Retoré, Christian

    Abstract | Document (2,443 KB) | BibTeX

    A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language
    Authors: Rodríguez, Leonardo ; Fridlender, Daniel ; Pagano, Miguel

    Abstract | Document (549 KB) | BibTeX

    Definitional Extension in Type Theory
    Authors: Xue, Tao

    Abstract | Document (549 KB) | BibTeX

    		  



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