23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@Proceedings{abel_et_al:LIPIcs.TYPES.2017, title = {{LIPIcs, Volume 104, TYPES'17, Complete Volume}}, booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-071-2}, ISSN = {1868-8969}, year = {2019}, volume = {104}, editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017}, URN = {urn:nbn:de:0030-drops-101671}, doi = {10.4230/LIPIcs.TYPES.2017}, annote = {Keywords: Theory of computation, Type theory, Proof theory, Program verification} }
23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{abel_et_al:LIPIcs.TYPES.2017.0, author = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)}, pages = {0:i--0:x}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-071-2}, ISSN = {1868-8969}, year = {2019}, volume = {104}, editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.0}, URN = {urn:nbn:de:0030-drops-100488}, doi = {10.4230/LIPIcs.TYPES.2017.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Guillaume Allais. Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 1:1-1:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{allais:LIPIcs.TYPES.2017.1, author = {Allais, Guillaume}, title = {{Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic}}, booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)}, pages = {1:1--1:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-071-2}, ISSN = {1868-8969}, year = {2019}, volume = {104}, editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.1}, URN = {urn:nbn:de:0030-drops-100490}, doi = {10.4230/LIPIcs.TYPES.2017.1}, annote = {Keywords: Type System, Bidirectional, Linear Logic, Agda} }
Andrej Dudenhefner and Jakob Rehof. Lower End of the Linial-Post Spectrum. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 2:1-2:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{dudenhefner_et_al:LIPIcs.TYPES.2017.2, author = {Dudenhefner, Andrej and Rehof, Jakob}, title = {{Lower End of the Linial-Post Spectrum}}, booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)}, pages = {2:1--2:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-071-2}, ISSN = {1868-8969}, year = {2019}, volume = {104}, editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.2}, URN = {urn:nbn:de:0030-drops-100503}, doi = {10.4230/LIPIcs.TYPES.2017.2}, annote = {Keywords: combinatory logic, lambda calculus, type theory, simple types, inhabitation, principal type} }
Herman Geuvers and Tonny Hurkens. Proof Terms for Generalized Natural Deduction. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 3:1-3:39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{geuvers_et_al:LIPIcs.TYPES.2017.3, author = {Geuvers, Herman and Hurkens, Tonny}, title = {{Proof Terms for Generalized Natural Deduction}}, booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)}, pages = {3:1--3:39}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-071-2}, ISSN = {1868-8969}, year = {2019}, volume = {104}, editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.3}, URN = {urn:nbn:de:0030-drops-100519}, doi = {10.4230/LIPIcs.TYPES.2017.3}, annote = {Keywords: constructive logic, natural deduction, detour conversion, permutation conversion, normalization Curry-Howard isomorphism} }
Rodolphe Lepigre. PML2: Integrated Program Verification in ML. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 4:1-4:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{lepigre:LIPIcs.TYPES.2017.4, author = {Lepigre, Rodolphe}, title = {{PML2: Integrated Program Verification in ML}}, booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)}, pages = {4:1--4:27}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-071-2}, ISSN = {1868-8969}, year = {2019}, volume = {104}, editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.4}, URN = {urn:nbn:de:0030-drops-100521}, doi = {10.4230/LIPIcs.TYPES.2017.4}, annote = {Keywords: program verification, classical logic, ML-like language, termination checking, Curry-style quantification, implicit subtyping} }
Julius Michaelis and Tobias Nipkow. Formalized Proof Systems for Propositional Logic. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{michaelis_et_al:LIPIcs.TYPES.2017.5, author = {Michaelis, Julius and Nipkow, Tobias}, title = {{Formalized Proof Systems for Propositional Logic}}, booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)}, pages = {5:1--5:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-071-2}, ISSN = {1868-8969}, year = {2019}, volume = {104}, editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.5}, URN = {urn:nbn:de:0030-drops-100537}, doi = {10.4230/LIPIcs.TYPES.2017.5}, annote = {Keywords: formalization of logic, proof systems, sequent calculus, natural deduction, resolution} }
Ian Orton and Andrew M. Pitts. Decomposing the Univalence Axiom. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{orton_et_al:LIPIcs.TYPES.2017.6, author = {Orton, Ian and Pitts, Andrew M.}, title = {{Decomposing the Univalence Axiom}}, booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)}, pages = {6:1--6:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-071-2}, ISSN = {1868-8969}, year = {2019}, volume = {104}, editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.6}, URN = {urn:nbn:de:0030-drops-100546}, doi = {10.4230/LIPIcs.TYPES.2017.6}, annote = {Keywords: dependent type theory, homotopy type theory, univalent type theory, univalence, cubical type theory, cubical sets} }
Erik Palmgren. On Equality of Objects in Categories in Constructive Type Theory. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 7:1-7:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{palmgren:LIPIcs.TYPES.2017.7, author = {Palmgren, Erik}, title = {{On Equality of Objects in Categories in Constructive Type Theory}}, booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)}, pages = {7:1--7:7}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-071-2}, ISSN = {1868-8969}, year = {2019}, volume = {104}, editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.7}, URN = {urn:nbn:de:0030-drops-100553}, doi = {10.4230/LIPIcs.TYPES.2017.7}, annote = {Keywords: type theory, formalization, category theory, setoids} }
Feedback for Dagstuhl Publishing