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} }
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} }
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} }
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} }
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} }
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} }
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} }
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} }
Feedback for Dagstuhl Publishing