@Proceedings{ghilezan_et_al:LIPIcs.TYPES.2016,
title = {{LIPIcs, Volume 97, TYPES'16, Complete Volume}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016},
URN = {urn:nbn:de:0030-drops-98651},
doi = {10.4230/LIPIcs.TYPES.2016},
annote = {Keywords: Theory of computation, Type theory}
}
@InProceedings{ghilezan_et_al:LIPIcs.TYPES.2016.0,
author = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {0:i--0:x},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.0},
URN = {urn:nbn:de:0030-drops-98466},
doi = {10.4230/LIPIcs.TYPES.2016.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
@InProceedings{miller:LIPIcs.TYPES.2016.1,
author = {Miller, Dale},
title = {{Mechanized Metatheory Revisited: An Extended Abstract}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {1:1--1:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.1},
URN = {urn:nbn:de:0030-drops-98603},
doi = {10.4230/LIPIcs.TYPES.2016.1},
annote = {Keywords: mechanized metatheory, mobility of binders, lambda-tree syntax, higher-order abstract syntax}
}
@InProceedings{ronchidellarocca:LIPIcs.TYPES.2016.2,
author = {Ronchi Della Rocca, Simona},
title = {{Intersection Types and Denotational Semantics: An Extended Abstract}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {2:1--2:7},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.2},
URN = {urn:nbn:de:0030-drops-98614},
doi = {10.4230/LIPIcs.TYPES.2016.2},
annote = {Keywords: Lambda-calculus, Lambda-models, Intersection types}
}
@InProceedings{adams_et_al:LIPIcs.TYPES.2016.3,
author = {Adams, Robin and Bezem, Marc and Coquand, Thierry},
title = {{A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {3:1--3:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.3},
URN = {urn:nbn:de:0030-drops-98581},
doi = {10.4230/LIPIcs.TYPES.2016.3},
annote = {Keywords: type theory, univalence, canonicity}
}
@InProceedings{aschieri_et_al:LIPIcs.TYPES.2016.4,
author = {Aschieri, Federico and Manighetti, Matteo},
title = {{On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {4:1--4:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.4},
URN = {urn:nbn:de:0030-drops-98590},
doi = {10.4230/LIPIcs.TYPES.2016.4},
annote = {Keywords: Markov's Principle, first-order logic, natural deduction, Curry-Howard}
}
@InProceedings{bauer_et_al:LIPIcs.TYPES.2016.5,
author = {Bauer, Andrej and Gilbert, Ga\"{e}tan and Haselwarter, Philipp G. and Pretnar, Matija and Stone, Christopher A.},
title = {{Design and Implementation of the Andromeda Proof Assistant}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {5:1--5:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.5},
URN = {urn:nbn:de:0030-drops-98574},
doi = {10.4230/LIPIcs.TYPES.2016.5},
annote = {Keywords: type theory, proof assistant, equality reflection, computational effects}
}
@InProceedings{bezem_et_al:LIPIcs.TYPES.2016.6,
author = {Bezem, Marc and Coquand, Thierry and Nakata, Keiko and Parmann, Erik},
title = {{Realizability at Work: Separating Two Constructive Notions of Finiteness}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {6:1--6:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.6},
URN = {urn:nbn:de:0030-drops-98541},
doi = {10.4230/LIPIcs.TYPES.2016.6},
annote = {Keywords: Type theory, realizability, constructive notions of finiteness}
}
@InProceedings{booij_et_al:LIPIcs.TYPES.2016.7,
author = {Booij, Auke B. and Escard\'{o}, Mart{\'\i}n H. and Lumsdaine, Peter LeFanu and Shulman, Michael},
title = {{Parametricity, Automorphisms of the Universe, and Excluded Middle}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {7:1--7:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.7},
URN = {urn:nbn:de:0030-drops-98554},
doi = {10.4230/LIPIcs.TYPES.2016.7},
annote = {Keywords: relational parametricity, dependent type theory, univalent foundations, homotopy type theory, excluded middle, classical mathematics, constructive mat}
}
@InProceedings{chrzaszcz_et_al:LIPIcs.TYPES.2016.8,
author = {Chrzaszcz, Jacek and Schubert, Aleksy and Zakrzewski, Jakub},
title = {{Coq Support in HAHA}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {8:1--8:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.8},
URN = {urn:nbn:de:0030-drops-98562},
doi = {10.4230/LIPIcs.TYPES.2016.8},
annote = {Keywords: Hoare logic, program verification, Coq theorem prover, teaching}
}
@InProceedings{czajka:LIPIcs.TYPES.2016.9,
author = {Czajka, Lukasz},
title = {{A Shallow Embedding of Pure Type Systems into First-Order Logic}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {9:1--9:39},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.9},
URN = {urn:nbn:de:0030-drops-98533},
doi = {10.4230/LIPIcs.TYPES.2016.9},
annote = {Keywords: pure type systems, first-order logic, hammers, proof automation, dependent type theory}
}
@InProceedings{espiritosanto_et_al:LIPIcs.TYPES.2016.10,
author = {Esp{\'\i}rito Santo, Jos\'{e} and Frade, Maria Jo\~{a}o and Pinto, Lu{\'\i}s},
title = {{Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {10:1--10:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.10},
URN = {urn:nbn:de:0030-drops-98523},
doi = {10.4230/LIPIcs.TYPES.2016.10},
annote = {Keywords: sequent calculus, permutative conversion, Curry-Howard isomorphism, vector of arguments, generalized application, normal proof, natural proof, cut eli}
}
@InProceedings{hou(favonia)_et_al:LIPIcs.TYPES.2016.11,
author = {Hou (Favonia), Kuen-Bang and Harper, Robert},
title = {{Covering Spaces in Homotopy Type Theory}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {11:1--11:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.11},
URN = {urn:nbn:de:0030-drops-98512},
doi = {10.4230/LIPIcs.TYPES.2016.11},
annote = {Keywords: homotopy type theory, covering space, fundamental group, mechanized reasoning}
}
@InProceedings{igried_et_al:LIPIcs.TYPES.2016.12,
author = {Igried, Bashar and Setzer, Anton},
title = {{Defining Trace Semantics for CSP-Agda}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {12:1--12:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.12},
URN = {urn:nbn:de:0030-drops-98509},
doi = {10.4230/LIPIcs.TYPES.2016.12},
annote = {Keywords: Agda, CSP, Coalgebras, Coinductive Data Types, Dependent Type Theory, IO-Monad, Induction-Recursion, Interactive Program, Monad, Monadic Programming,}
}
@InProceedings{lungu_et_al:LIPIcs.TYPES.2016.13,
author = {Lungu, Georgiana Elena and Luo, Zhaohui},
title = {{On Subtyping in Type Theories with Canonical Objects}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {13:1--13:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.13},
URN = {urn:nbn:de:0030-drops-98496},
doi = {10.4230/LIPIcs.TYPES.2016.13},
annote = {Keywords: subtyping, type theory, conservative extension, canonical objects}
}
@InProceedings{martindorel_et_al:LIPIcs.TYPES.2016.14,
author = {Martin-Dorel, \'{E}rik and Soloviev, Sergei},
title = {{A Formal Study of Boolean Games with Random Formulas as Payoff Functions}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {14:1--14:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.14},
URN = {urn:nbn:de:0030-drops-98486},
doi = {10.4230/LIPIcs.TYPES.2016.14},
annote = {Keywords: Boolean games, Random process, Coq formal proofs}
}
@InProceedings{statman:LIPIcs.TYPES.2016.15,
author = {Statman, Richard},
title = {{The Completeness of BCD for an Operational Semantics}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {15:1--15:5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.15},
URN = {urn:nbn:de:0030-drops-98478},
doi = {10.4230/LIPIcs.TYPES.2016.15},
annote = {Keywords: intersection types, operational semantics, Beth model, logical relations, forcing}
}
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