LIPIcs, Volume 39
TYPES 2014, May 12-15, 2014, Paris, France
Editors: Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@Proceedings{herbelin_et_al:LIPIcs.TYPES.2014, title = {{LIPIcs, Volume 39, TYPES'14, Complete Volume}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014}, URN = {urn:nbn:de:0030-drops-55047}, doi = {10.4230/LIPIcs.TYPES.2014}, annote = {Keywords: Applicative (Functional) Programming, Software/Program Verification, Specifying and Verifying and Reasoning about Programs, Mathematical Logic} }
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. i-x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{herbelin_et_al:LIPIcs.TYPES.2014.i, author = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, title = {{Front Matter, Table of Contents, Preface, Authors Index}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {i--x}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.i}, URN = {urn:nbn:de:0030-drops-54888}, doi = {10.4230/LIPIcs.TYPES.2014.i}, annote = {Keywords: Front Matter, Table of Contents, Preface, Authors Index} }
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Benedikt Ahrens and Régis Spadotti. Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 1-26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{ahrens_et_al:LIPIcs.TYPES.2014.1, author = {Ahrens, Benedikt and Spadotti, R\'{e}gis}, title = {{Terminal Semantics for Codata Types in Intensional Martin-L\"{o}f Type Theory}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {1--26}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.1}, URN = {urn:nbn:de:0030-drops-54891}, doi = {10.4230/LIPIcs.TYPES.2014.1}, annote = {Keywords: relative comonad, Martin-L\"{o}f type theory, coinductive type, computer theorem proving} }
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Ali Assaf. A Calculus of Constructions with Explicit Subtyping. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 27-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{assaf:LIPIcs.TYPES.2014.27, author = {Assaf, Ali}, title = {{A Calculus of Constructions with Explicit Subtyping}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {27--46}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.27}, URN = {urn:nbn:de:0030-drops-54904}, doi = {10.4230/LIPIcs.TYPES.2014.27}, annote = {Keywords: type theory, calculus of constructions, universes, cumulativity, subtyping} }
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Raphaël Cauderlier and Catherine Dubois. Objects and Subtyping in the Lambda-Pi-Calculus Modulo. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 47-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{cauderlier_et_al:LIPIcs.TYPES.2014.47, author = {Cauderlier, Rapha\"{e}l and Dubois, Catherine}, title = {{Objects and Subtyping in the Lambda-Pi-Calculus Modulo}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {47--71}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.47}, URN = {urn:nbn:de:0030-drops-54919}, doi = {10.4230/LIPIcs.TYPES.2014.47}, annote = {Keywords: object, calculus, encoding, dependent type, rewrite system} }
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Olivier Danvy, Chantal Keller, and Matthias Puech. Typeful Normalization by Evaluation. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 72-88, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{danvy_et_al:LIPIcs.TYPES.2014.72, author = {Danvy, Olivier and Keller, Chantal and Puech, Matthias}, title = {{Typeful Normalization by Evaluation}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {72--88}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.72}, URN = {urn:nbn:de:0030-drops-54921}, doi = {10.4230/LIPIcs.TYPES.2014.72}, annote = {Keywords: Normalization by Evaluation, Generalized Algebraic Data Types, Continuation-Passing Style, partial evaluation} }
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Jules Hedges. Dialectica Categories and Games with Bidding. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 89-110, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{hedges:LIPIcs.TYPES.2014.89, author = {Hedges, Jules}, title = {{Dialectica Categories and Games with Bidding}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {89--110}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.89}, URN = {urn:nbn:de:0030-drops-54937}, doi = {10.4230/LIPIcs.TYPES.2014.89}, annote = {Keywords: Linear logic, Dialectica categories, categorical semantics, model theory, game semantics, dependent types, functional interpretations} }
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Nicolai Kraus. The General Universal Property of the Propositional Truncation. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 111-145, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{kraus:LIPIcs.TYPES.2014.111, author = {Kraus, Nicolai}, title = {{The General Universal Property of the Propositional Truncation}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {111--145}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.111}, URN = {urn:nbn:de:0030-drops-54944}, doi = {10.4230/LIPIcs.TYPES.2014.111}, annote = {Keywords: coherence conditions, propositional truncation, Reedy limits, universal property, well-behaved constancy} }
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Jean-Louis Krivine. On the Structure of Classical Realizability Models of ZF. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 146-161, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{krivine:LIPIcs.TYPES.2014.146, author = {Krivine, Jean-Louis}, title = {{On the Structure of Classical Realizability Models of ZF}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {146--161}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.146}, URN = {urn:nbn:de:0030-drops-54953}, doi = {10.4230/LIPIcs.TYPES.2014.146}, annote = {Keywords: lambda-calculus, Curry-Howard correspondence, set theory} }
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Maria Emilia Maietti and Samuele Maschio. An Extensional Kleene Realizability Semantics for the Minimalist Foundation. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 162-186, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{maietti_et_al:LIPIcs.TYPES.2014.162, author = {Maietti, Maria Emilia and Maschio, Samuele}, title = {{An Extensional Kleene Realizability Semantics for the Minimalist Foundation}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {162--186}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.162}, URN = {urn:nbn:de:0030-drops-54966}, doi = {10.4230/LIPIcs.TYPES.2014.162}, annote = {Keywords: Realizability, Type Theory, formal Church Thesis} }
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Erik Parmann. Investigating Streamless Sets. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 187-201, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{parmann:LIPIcs.TYPES.2014.187, author = {Parmann, Erik}, title = {{Investigating Streamless Sets}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {187--201}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.187}, URN = {urn:nbn:de:0030-drops-54971}, doi = {10.4230/LIPIcs.TYPES.2014.187}, annote = {Keywords: Type theory, Constructive Logic, Finite Sets} }
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Andrew M. Pitts. Nominal Presentation of Cubical Sets Models of Type Theory. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 202-220, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{pitts:LIPIcs.TYPES.2014.202, author = {Pitts, Andrew M.}, title = {{Nominal Presentation of Cubical Sets Models of Type Theory}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {202--220}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.202}, URN = {urn:nbn:de:0030-drops-54980}, doi = {10.4230/LIPIcs.TYPES.2014.202}, annote = {Keywords: models of dependent type theory, homotopy type theory, cubical sets, nominal sets, monoids} }
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Andrew Polonsky. Extensionality of lambda-*. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 221-250, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{polonsky:LIPIcs.TYPES.2014.221, author = {Polonsky, Andrew}, title = {{Extensionality of lambda-*}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {221--250}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.221}, URN = {urn:nbn:de:0030-drops-54995}, doi = {10.4230/LIPIcs.TYPES.2014.221}, annote = {Keywords: Extensionality, logical relations, type theory, lambda calculus, reflection} }
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Aleksy Schubert, Pawel Urzyczyn, and Daria Walukiewicz-Chrzaszcz. Restricted Positive Quantification Is Not Elementary. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 251-273, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{schubert_et_al:LIPIcs.TYPES.2014.251, author = {Schubert, Aleksy and Urzyczyn, Pawel and Walukiewicz-Chrzaszcz, Daria}, title = {{Restricted Positive Quantification Is Not Elementary}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {251--273}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.251}, URN = {urn:nbn:de:0030-drops-55002}, doi = {10.4230/LIPIcs.TYPES.2014.251}, annote = {Keywords: constructive logic, complexity, automata theory} }
Feedback for Dagstuhl Publishing