LIPIcs, Volume 303
TYPES 2023, June 12-16, 2023, ETSInf, Universitat Politècnica de València, Spain
Editors: Delia Kesner, Eduardo Hermo Reyes, and Benno van den Berg
LIPIcs, Volume 269
TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France
Editors: Delia Kesner and Pierre-Marie Pédrot
LIPIcs, Volume 52
FSCD 2016, June 22-26, 2016, Porto, Portugal
Editors: Delia Kesner and Brigitte Pientka
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Dennis Hilhorst and Paige Randall North. Formalizing the Algebraic Small Object Argument in UniMath. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{hilhorst_et_al:LIPIcs.ITP.2024.20, author = {Hilhorst, Dennis and North, Paige Randall}, title = {{Formalizing the Algebraic Small Object Argument in UniMath}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {20:1--20:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.20}, URN = {urn:nbn:de:0030-drops-207486}, doi = {10.4230/LIPIcs.ITP.2024.20}, annote = {Keywords: formalization of mathematics, univalent foundations, model category theory, algebraic small object argument, coq, unimath} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Dohan Kim. An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kim:LIPIcs.ITP.2024.24, author = {Kim, Dohan}, title = {{An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {24:1--24:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.24}, URN = {urn:nbn:de:0030-drops-207525}, doi = {10.4230/LIPIcs.ITP.2024.24}, annote = {Keywords: Narrowing, Multiset Narrowing, Unifiability, Reachability} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Max Zeuner and Matthias Hutzler. The Functor of Points Approach to Schemes in Cubical Agda. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 38:1-38:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{zeuner_et_al:LIPIcs.ITP.2024.38, author = {Zeuner, Max and Hutzler, Matthias}, title = {{The Functor of Points Approach to Schemes in Cubical Agda}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {38:1--38:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.38}, URN = {urn:nbn:de:0030-drops-207667}, doi = {10.4230/LIPIcs.ITP.2024.38}, annote = {Keywords: Schemes, Algebraic Geometry, Category Theory, Cubical Agda, Homotopy Type Theory and Univalent Foundations, Constructive Mathematics} }
Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)
29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 1-138, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@Proceedings{kesner_et_al:LIPIcs.TYPES.2023, title = {{LIPIcs, Volume 303, TYPES 2023, Complete Volume}}, booktitle = {29th International Conference on Types for Proofs and Programs (TYPES 2023)}, pages = {1--138}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-332-4}, ISSN = {1868-8969}, year = {2024}, volume = {303}, editor = {Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023}, URN = {urn:nbn:de:0030-drops-204778}, doi = {10.4230/LIPIcs.TYPES.2023}, annote = {Keywords: LIPIcs, Volume 303, TYPES 2023, Complete Volume} }
Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)
29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 0:i-0:viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kesner_et_al:LIPIcs.TYPES.2023.0, author = {Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {29th International Conference on Types for Proofs and Programs (TYPES 2023)}, pages = {0:i--0:viii}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-332-4}, ISSN = {1868-8969}, year = {2024}, volume = {303}, editor = {Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.0}, URN = {urn:nbn:de:0030-drops-204787}, doi = {10.4230/LIPIcs.TYPES.2023.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)
Jelle Wemmenhove, Cosmin Manea, and Jim Portegies. Classification of Covering Spaces and Canonical Change of Basepoint. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 1:1-1:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{wemmenhove_et_al:LIPIcs.TYPES.2023.1, author = {Wemmenhove, Jelle and Manea, Cosmin and Portegies, Jim}, title = {{Classification of Covering Spaces and Canonical Change of Basepoint}}, booktitle = {29th International Conference on Types for Proofs and Programs (TYPES 2023)}, pages = {1:1--1:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-332-4}, ISSN = {1868-8969}, year = {2024}, volume = {303}, editor = {Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.1}, URN = {urn:nbn:de:0030-drops-204795}, doi = {10.4230/LIPIcs.TYPES.2023.1}, annote = {Keywords: Synthetic Homotopy Theory, Homotopy Type Theory, Covering Spaces, Change-of-Basepoint Isomorphism} }
Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)
Andrej Dudenhefner, Christoph Stahl, Constantin Chaumet, Felix Laarmann, and Jakob Rehof. Finite Combinatory Logic with Predicates. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 2:1-2:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{dudenhefner_et_al:LIPIcs.TYPES.2023.2, author = {Dudenhefner, Andrej and Stahl, Christoph and Chaumet, Constantin and Laarmann, Felix and Rehof, Jakob}, title = {{Finite Combinatory Logic with Predicates}}, booktitle = {29th International Conference on Types for Proofs and Programs (TYPES 2023)}, pages = {2:1--2:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-332-4}, ISSN = {1868-8969}, year = {2024}, volume = {303}, editor = {Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.2}, URN = {urn:nbn:de:0030-drops-204808}, doi = {10.4230/LIPIcs.TYPES.2023.2}, annote = {Keywords: combinatory logic, inhabitation, intersection types, program synthesis} }
Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)
Greta Coraglia and Jacopo Emmenegger. Categorical Models of Subtyping. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{coraglia_et_al:LIPIcs.TYPES.2023.3, author = {Coraglia, Greta and Emmenegger, Jacopo}, title = {{Categorical Models of Subtyping}}, booktitle = {29th International Conference on Types for Proofs and Programs (TYPES 2023)}, pages = {3:1--3:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-332-4}, ISSN = {1868-8969}, year = {2024}, volume = {303}, editor = {Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.3}, URN = {urn:nbn:de:0030-drops-204811}, doi = {10.4230/LIPIcs.TYPES.2023.3}, annote = {Keywords: dependent types, subtyping, coercive subtyping, categorical semantics, categories with families, monad} }
Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)
Joris Ceulemans, Andreas Nuyts, and Dominique Devriese. A Sound and Complete Substitution Algorithm for Multimode Type Theory. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{ceulemans_et_al:LIPIcs.TYPES.2023.4, author = {Ceulemans, Joris and Nuyts, Andreas and Devriese, Dominique}, title = {{A Sound and Complete Substitution Algorithm for Multimode Type Theory}}, booktitle = {29th International Conference on Types for Proofs and Programs (TYPES 2023)}, pages = {4:1--4:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-332-4}, ISSN = {1868-8969}, year = {2024}, volume = {303}, editor = {Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.4}, URN = {urn:nbn:de:0030-drops-204826}, doi = {10.4230/LIPIcs.TYPES.2023.4}, annote = {Keywords: dependent type theory, modalities, multimode type theory, explicit substitutions, substitution algorithm} }
Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)
Michał J. Gajda. Consistent Ultrafinitist Logic. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{gajda:LIPIcs.TYPES.2023.5, author = {Gajda, Micha{\l} J.}, title = {{Consistent Ultrafinitist Logic}}, booktitle = {29th International Conference on Types for Proofs and Programs (TYPES 2023)}, pages = {5:1--5:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-332-4}, ISSN = {1868-8969}, year = {2024}, volume = {303}, editor = {Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.5}, URN = {urn:nbn:de:0030-drops-204833}, doi = {10.4230/LIPIcs.TYPES.2023.5}, annote = {Keywords: ultrafinitism, bounded Turing completeness, logic of computability, decidable logic, explicit complexity, strict finitism} }
Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)
Matthias Eberl. A Reflection Principle for Potential Infinite Models of Type Theory. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{eberl:LIPIcs.TYPES.2023.6, author = {Eberl, Matthias}, title = {{A Reflection Principle for Potential Infinite Models of Type Theory}}, booktitle = {29th International Conference on Types for Proofs and Programs (TYPES 2023)}, pages = {6:1--6:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-332-4}, ISSN = {1868-8969}, year = {2024}, volume = {303}, editor = {Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.6}, URN = {urn:nbn:de:0030-drops-204845}, doi = {10.4230/LIPIcs.TYPES.2023.6}, annote = {Keywords: Indefinite extensibility, Potential infinite, Reflection principle} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Niels van der Weide. Univalent Enriched Categories and the Enriched Rezk Completion. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{vanderweide:LIPIcs.FSCD.2024.4, author = {van der Weide, Niels}, title = {{Univalent Enriched Categories and the Enriched Rezk Completion}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {4:1--4:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.4}, URN = {urn:nbn:de:0030-drops-203337}, doi = {10.4230/LIPIcs.FSCD.2024.4}, annote = {Keywords: enriched categories, univalent categories, homotopy type theory, univalent foundations, Rezk completion} }
Feedback for Dagstuhl Publishing