Volume
LIPIcs, Volume 303
29th International Conference on Types for Proofs and Programs (TYPES 2023)
Publication Details
- published at: 2024-08-20
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-332-4
- DBLP: db/conf/types/types2023
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 303, TYPES 2023, Complete Volume
Abstract
LIPIcs, Volume 303, TYPES 2023, Complete Volume
Cite as
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)
Copy BibTex To Clipboard
@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}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
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)
Copy BibTex To Clipboard
@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}
}
Document
Classification of Covering Spaces and Canonical Change of Basepoint
Abstract
Using the language of homotopy type theory (HoTT), we 1) prove a synthetic version of the classification theorem for covering spaces, and 2) explore the existence of canonical change-of-basepoint isomorphisms between homotopy groups. There is some freedom in choosing how to translate concepts from classical algebraic topology into HoTT. The final translations we ended up with are easier to work with than the ones we started with. We discuss some earlier attempts to shed light on this translation process. The proofs are mechanized using the Coq proof assistant and closely follow classical treatments like those by Hatcher [Allen Hatcher, 2002].
Cite as
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)
Copy BibTex To Clipboard
@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}
}
Document
Finite Combinatory Logic with Predicates
Abstract
Type inhabitation in extensions of Finite Combinatory Logic (FCL) is the mechanism underlying various component-oriented synthesis frameworks. In FCL inhabitant sets correspond to regular tree languages and vice versa. Therefore, it is not possible to specify non-regular properties of inhabitants, such as (dis)equality of subterms. Additionally, the monomorphic nature of FCL oftentimes hinders concise specification of components.
We propose a conservative extension to FCL by quantifiers and predicates, introducing a restricted form of polymorphism. In the proposed type system (FCLP) inhabitant sets correspond to decidable term languages and vice versa. As a consequence, type inhabitation in FCLP is undecidable. Based on results in tree automata theory, we identify a fragment of FCLP with the following two properties. First, the fragment enjoys decidable type inhabitation. Second, it allows for specification of local (dis)equality constraints for subterms of inhabitants.
For empirical evaluation, we implement a semi-decision procedure for type inhabitation in FCLP. We compare specification capabilities, scalability, and performance of the implementation to existing FCL-based approaches. Finally, we evaluate practical applicability via a case study, synthesizing mechanically sound robotic arms.
Cite as
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)
Copy BibTex To Clipboard
@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}
}
Document
Categorical Models of Subtyping
Abstract
Most categorical models for dependent types have traditionally been heavily set based: contexts form a category, and for each we have a set of types in said context - and for each type a set of terms of said type. This is the case for categories with families, categories with attributes, and natural models; in particular, all of them can be traced back to certain discrete Grothendieck fibrations. We extend this intuition to the case of general, not necessarily discrete, fibrations, so that over a given context one has not only a set but a category of types.
We argue that the added structure can be attributed to a notion of subtyping that shares many features with that of coercive subtyping, in the sense that it is the product of thinking about subtyping as an abbreviation mechanism: we say that a given type A' is a subtype of A if there is a unique coercion from A' to A. Whenever we need a term of type A, then, it suffices to have a term of type A', which we can "plug-in" into A.
For this version of subtyping we provide rules, coherences, and explicit models, and we compare and contrast it to coercive subtyping as introduced by Z. Luo and others. We conclude by suggesting how the tools we present can be employed in finding appropriate rules relating subtyping and certain type constructors.
Cite as
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)
Copy BibTex To Clipboard
@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}
}
Document
A Sound and Complete Substitution Algorithm for Multimode Type Theory
Abstract
Multimode Type Theory (MTT) is a generic type theory that can be instantiated with an arbitrary mode theory to model features like parametricity, cohesion and guarded recursion. However, the presence of modalities in MTT significantly complicates the substitution calculus of this system. Moreover, MTT’s syntax has explicit substitutions with an axiomatic system - not an algorithm - governing the connection between an explicitly substituted term and the resulting term in which variables have actually been replaced. So far, the only results on eliminating explicit substitutions in MTT rely on normalisation by evaluation and hence also immediately normalise a term. In this paper, we present a substitution algorithm for MTT that is completely separated from normalisation. To this end, we introduce Substitution-Free Multimode Type Theory (SFMTT): a formulation of MTT without explicit substitutions, but for which we are able to give a structurally recursive substitution algorithm, suitable for implementation in a total programming language or proof assistant. On the usual formulation of MTT, we consider σ-equality, the congruence generated solely by equality rules for explicit substitutions. There is a trivial embedding from SFMTT to MTT, and a converse translation that eliminates the explicit substitutions. We prove soundness and completeness of our algorithm with respect to σ-equivalence and thus establish that MTT with σ-equality has computable σ-normal forms, given by the terms of SFMTT.
Cite as
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)
Copy BibTex To Clipboard
@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}
}
Document
Consistent Ultrafinitist Logic
Abstract
Ultrafinitism postulates that we can only compute on relatively short objects, and numbers beyond a certain value are not available. This approach would also forbid many forms of infinitary reasoning and allow removing certain paradoxes stemming from enumeration theorems. For a computational application of ultrafinitist logic, we need more than a proof system, but a logical framework to express both proofs, programs, and theorems in a single framework. We present its inference rules, reduction relation, and self-encoding to allow direct proving of the properties of ultrafinitist logic within itself. We also provide a justification why it can express all bounded Turing programs, and thus serve as a "logic of computability".
Cite as
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)
Copy BibTex To Clipboard
@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}
}
Document
A Reflection Principle for Potential Infinite Models of Type Theory
Abstract
Denotational models of type theory, such as set-theoretic, domain-theoretic, or category-theoretic models use (actual) infinite sets of objects in one way or another. The potential infinite, seen as an extensible finite, requires a dynamic understanding of the infinite sets of objects. It follows that the type nat cannot be interpreted as a set of all natural numbers, [[nat]] = ℕ, but as an increasing family of finite sets ℕ_i = {0, … , i-1}. Any reference to [[nat]], either by the formal syntax or by meta-level concepts, must be a reference to a (sufficiently large) set ℕ_i.
We present the basic concepts for interpreting a fragment of the simply typed λ-calculus within such a dynamic model. A type ϱ is thereby interpreted as a process, which is formally a factor system together with a limit of it. A factor system is very similar to a direct or an inverse system, and its limit is also defined by a universal property. It is crucial to recognize that a limit is not necessarily an unreachable end beyond the process. Rather, it can be regarded as an intermediate state within the factor system, which can still be extended.
The logical type bool plays an important role, which we interpret classically as the set {true, false}. We provide an interpretation of simply typed λ-terms in these factor systems and limits. The main result is a reflection principle, which states that an element in the limit has a "full representative" at a sufficiently large stage within the factor system. For propositions, that is, terms of type bool, this implies that statements about the limit are true if and only if they are true at that sufficiently large stage.
Cite as
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)
Copy BibTex To Clipboard
@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}
}