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} }
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} }
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} }
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} }
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} }
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} }
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} }
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} }
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} }
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} }
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} }
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} }
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} }
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} }
Sergei Soloviev. On Isomorphism of Dependent Products in a Typed Logical Framework. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 274-287, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{soloviev:LIPIcs.TYPES.2014.274, author = {Soloviev, Sergei}, title = {{On Isomorphism of Dependent Products in a Typed Logical Framework}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {274--287}, 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.274}, URN = {urn:nbn:de:0030-drops-55013}, doi = {10.4230/LIPIcs.TYPES.2014.274}, annote = {Keywords: Isomorphism of types, dependent product, logical framework} }
Silvia Steila. An Intuitionistic Analysis of Size-change Termination. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 288-307, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{steila:LIPIcs.TYPES.2014.288, author = {Steila, Silvia}, title = {{An Intuitionistic Analysis of Size-change Termination}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {288--307}, 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.288}, URN = {urn:nbn:de:0030-drops-55026}, doi = {10.4230/LIPIcs.TYPES.2014.288}, annote = {Keywords: Intuitionism, Ramsey's Theorem, Termination} }
Feedback for Dagstuhl Publishing