LIPIcs, Volume 104
TYPES 2017, May 29 to June 1, 2017, Budapest, Hungary
Editors: Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi
Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)
Georgi Nakov and Fredrik Nordvall Forsberg. Quantitative Polynomial Functors. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{nakov_et_al:LIPIcs.TYPES.2021.10, author = {Nakov, Georgi and Nordvall Forsberg, Fredrik}, title = {{Quantitative Polynomial Functors}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {10:1--10:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.10}, URN = {urn:nbn:de:0030-drops-167795}, doi = {10.4230/LIPIcs.TYPES.2021.10}, annote = {Keywords: quantitative type theory, polynomial functors, inductive data types} }
Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)
Georgi Nakov and Fredrik Nordvall Forsberg. Quantitative Polynomial Functors (Early Ideas). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 22:1-22:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{nakov_et_al:LIPIcs.CALCO.2021.22, author = {Nakov, Georgi and Nordvall Forsberg, Fredrik}, title = {{Quantitative Polynomial Functors}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {22:1--22:5}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.22}, URN = {urn:nbn:de:0030-drops-153774}, doi = {10.4230/LIPIcs.CALCO.2021.22}, annote = {Keywords: quantitative type theory, polynomial functors, inductive data types} }
Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)
Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu. Connecting Constructive Notions of Ordinals in Homotopy Type Theory. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 70:1-70:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{kraus_et_al:LIPIcs.MFCS.2021.70, author = {Kraus, Nicolai and Nordvall Forsberg, Fredrik and Xu, Chuangjie}, title = {{Connecting Constructive Notions of Ordinals in Homotopy Type Theory}}, booktitle = {46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)}, pages = {70:1--70:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-201-3}, ISSN = {1868-8969}, year = {2021}, volume = {202}, editor = {Bonchi, Filippo and Puglisi, Simon J.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.70}, URN = {urn:nbn:de:0030-drops-145100}, doi = {10.4230/LIPIcs.MFCS.2021.70}, annote = {Keywords: Constructive ordinals, Cantor normal forms, Brouwer trees} }
Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Ambrus Kaposi, András Kovács, and Ambroise Lafont. For Finitary Induction-Induction, Induction Is Enough. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 6:1-6:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{kaposi_et_al:LIPIcs.TYPES.2019.6, author = {Kaposi, Ambrus and Kov\'{a}cs, Andr\'{a}s and Lafont, Ambroise}, title = {{For Finitary Induction-Induction, Induction Is Enough}}, booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)}, pages = {6:1--6:30}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-158-0}, ISSN = {1868-8969}, year = {2020}, volume = {175}, editor = {Bezem, Marc and Mahboubi, Assia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.6}, URN = {urn:nbn:de:0030-drops-130707}, doi = {10.4230/LIPIcs.TYPES.2019.6}, annote = {Keywords: type theory, inductive types, inductive-inductive types} }
Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
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-dev.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} }
Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
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-dev.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} }
Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
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-dev.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} }
Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
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-dev.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} }
Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
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-dev.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} }
Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
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-dev.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} }
Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
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-dev.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} }
Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
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-dev.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} }
Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
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-dev.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} }
Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)
Neil Ghani, Conor McBride, Fredrik Nordvall Forsberg, and Stephan Spahn. Variations on Inductive-Recursive Definitions. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 63:1-63:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{ghani_et_al:LIPIcs.MFCS.2017.63, author = {Ghani, Neil and McBride, Conor and Nordvall Forsberg, Fredrik and Spahn, Stephan}, title = {{Variations on Inductive-Recursive Definitions}}, booktitle = {42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)}, pages = {63:1--63:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-046-0}, ISSN = {1868-8969}, year = {2017}, volume = {83}, editor = {Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.63}, URN = {urn:nbn:de:0030-drops-81184}, doi = {10.4230/LIPIcs.MFCS.2017.63}, annote = {Keywords: Type Theory, induction-recursion, initial-algebra semantics} }
Feedback for Dagstuhl Publishing