@Proceedings{dybjer_et_al:LIPIcs.TYPES.2018,
title = {{LIPIcs, Volume 130, TYPES'18, Complete Volume}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018},
URN = {urn:nbn:de:0030-drops-114507},
doi = {10.4230/LIPIcs.TYPES.2018},
annote = {Keywords: Theory of computation,Type theory; Constructive mathematics; Logic and verification; Program verification, Software and its engineering}
}
@InProceedings{dybjer_et_al:LIPIcs.TYPES.2018.0,
author = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
pages = {0:i--0:x},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.0},
URN = {urn:nbn:de:0030-drops-114045},
doi = {10.4230/LIPIcs.TYPES.2018.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
@InProceedings{berger_et_al:LIPIcs.TYPES.2018.1,
author = {Berger, Ulrich and Matthes, Ralph and Setzer, Anton},
title = {{Martin Hofmann’s Case for Non-Strictly Positive Data Types}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
pages = {1:1--1:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.1},
URN = {urn:nbn:de:0030-drops-114052},
doi = {10.4230/LIPIcs.TYPES.2018.1},
annote = {Keywords: non strictly-positive data types, breadth-first traversal, program verification, Mendler-style recursion, System F, theorem proving, Coq, Agda, Haskell}
}
@InProceedings{dudenhefner_et_al:LIPIcs.TYPES.2018.2,
author = {Dudenhefner, Andrej and Rehof, Jakob},
title = {{A Simpler Undecidability Proof for System F Inhabitation}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
pages = {2:1--2:11},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.2},
URN = {urn:nbn:de:0030-drops-114061},
doi = {10.4230/LIPIcs.TYPES.2018.2},
annote = {Keywords: System F, Lambda Calculus, Inhabitation, Propositional Logic, Provability, Undecidability, Coq, Formalization}
}
@InProceedings{petrakis:LIPIcs.TYPES.2018.3,
author = {Petrakis, Iosif},
title = {{Dependent Sums and Dependent Products in Bishop’s Set Theory}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
pages = {3:1--3:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.3},
URN = {urn:nbn:de:0030-drops-114070},
doi = {10.4230/LIPIcs.TYPES.2018.3},
annote = {Keywords: Bishop’s constructive mathematics, Martin-L\"{o}f’s type theory, dependent sums, dependent products, type-theoretic axiom of choice}
}
@InProceedings{petrucciani_et_al:LIPIcs.TYPES.2018.4,
author = {Petrucciani, Tommaso and Castagna, Giuseppe and Ancona, Davide and Zucca, Elena},
title = {{Semantic Subtyping for Non-Strict Languages}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
pages = {4:1--4:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.4},
URN = {urn:nbn:de:0030-drops-114083},
doi = {10.4230/LIPIcs.TYPES.2018.4},
annote = {Keywords: Semantic subtyping, non-strict semantics, call-by-need, union types, intersection types}
}
@InProceedings{schlichtkrull:LIPIcs.TYPES.2018.5,
author = {Schlichtkrull, Anders},
title = {{New Formalized Results on the Meta-Theory of a Paraconsistent Logic}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
pages = {5:1--5:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.5},
URN = {urn:nbn:de:0030-drops-114098},
doi = {10.4230/LIPIcs.TYPES.2018.5},
annote = {Keywords: Paraconsistent logic, Many-valued logic, Formalization, Isabelle proof assistant, Paraconsistency}
}
@InProceedings{sestini:LIPIcs.TYPES.2018.6,
author = {Sestini, Filippo},
title = {{Normalization by Evaluation for Typed Weak lambda-Reduction}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
pages = {6:1--6:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.6},
URN = {urn:nbn:de:0030-drops-114101},
doi = {10.4230/LIPIcs.TYPES.2018.6},
annote = {Keywords: normalization, lambda-calculus, reduction, term-rewriting, Agda}
}
@InProceedings{uemura:LIPIcs.TYPES.2018.7,
author = {Uemura, Taichi},
title = {{Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
pages = {7:1--7:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.7},
URN = {urn:nbn:de:0030-drops-114118},
doi = {10.4230/LIPIcs.TYPES.2018.7},
annote = {Keywords: Cubical type theory, Realizability, Impredicative universe, Univalence, Propositional resizing}
}
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