@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
The metadata provided by Dagstuhl Publishing on its webpages, as well as their export formats (such as XML or BibTeX) available at our website, is released under the CC0 1.0 Public Domain Dedication license. That is, you are free to copy, distribute, use, modify, transform, build upon, and produce derived works from our data, even for commercial purposes, all without asking permission. Of course, we are always happy if you provide a link to us as the source of the data.
Read the full CC0 1.0 legal code for the exact terms that apply: https://creativecommons.org/publicdomain/zero/1.0/legalcode
Feedback for Dagstuhl Publishing