LIPIcs, Volume 97
TYPES 2016, May 23-26, 2016, Novi Sad, Serbia
Editors: Silvia Ghilezan, Herman Geuvers, and Jelena Ivetic
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
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-dev.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} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
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-dev.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} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
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-dev.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} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
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-dev.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} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
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-dev.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} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
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-dev.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} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
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-dev.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} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
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-dev.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} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
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-dev.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} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
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-dev.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} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
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-dev.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} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
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-dev.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} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
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-dev.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} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
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,} }
Feedback for Dagstuhl Publishing