22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Dale Miller. Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper). In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 1:1-1:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Simona Ronchi Della Rocca. Intersection Types and Denotational Semantics: An Extended Abstract (Invited Paper). In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 2:1-2:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Robin Adams, Marc Bezem, and Thierry Coquand. A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 3:1-3:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Federico Aschieri and Matteo Manighetti. On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, and Christopher A. Stone. Design and Implementation of the Andromeda Proof Assistant. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 5:1-5:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Marc Bezem, Thierry Coquand, Keiko Nakata, and Erik Parmann. Realizability at Work: Separating Two Constructive Notions of Finiteness. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Auke B. Booij, Martín H. Escardó, Peter LeFanu Lumsdaine, and Michael Shulman. Parametricity, Automorphisms of the Universe, and Excluded Middle. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 7:1-7:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Jacek Chrzaszcz, Aleksy Schubert, and Jakub Zakrzewski. Coq Support in HAHA. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 8:1-8:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Lukasz Czajka. A Shallow Embedding of Pure Type Systems into First-Order Logic. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 9:1-9:39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
José Espírito Santo, Maria João Frade, and Luís Pinto. Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 10:1-10:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Kuen-Bang Hou (Favonia) and Robert Harper. Covering Spaces in Homotopy Type Theory. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Bashar Igried and Anton Setzer. Defining Trace Semantics for CSP-Agda. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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,} }
Georgiana Elena Lungu and Zhaohui Luo. On Subtyping in Type Theories with Canonical Objects. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 13:1-13:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Érik Martin-Dorel and Sergei Soloviev. A Formal Study of Boolean Games with Random Formulas as Payoff Functions. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 14:1-14:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }
Richard Statman. The Completeness of BCD for an Operational Semantics. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 15:1-15:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@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} }