Volume
LIPIcs, Volume 337
10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD)
Event
FSCD 2025, July 14-20, 2025, Birmingham, UKEditor
Publication Details
- published at: 2025-07-07
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-374-4
- DBLP: db/conf/fscd/fscd2025
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 337, FSCD 2025, Complete Volume
Abstract
LIPIcs, Volume 337, FSCD 2025, Complete Volume
Cite as
10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 1-724, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Proceedings{fernandez:LIPIcs.FSCD.2025,
title = {{LIPIcs, Volume 337, FSCD 2025, Complete Volume}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {1--724},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025},
URN = {urn:nbn:de:0030-drops-237821},
doi = {10.4230/LIPIcs.FSCD.2025},
annote = {Keywords: LIPIcs, Volume 337, FSCD 2025, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{fernandez:LIPIcs.FSCD.2025.0,
author = {Fern\'{a}ndez, Maribel},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {0:i--0:xviii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.0},
URN = {urn:nbn:de:0030-drops-237819},
doi = {10.4230/LIPIcs.FSCD.2025.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Computation First: Rebuilding Constructivism with Effects (Invited Talk)
Abstract
Constructive logic and type theory have traditionally been grounded in pure, effect-free model of computation. This paper argues that such a restriction is not a foundational necessity but a historical artifact, and it advocates for a broader perspective of effectful constructivism, where computational effects, such as state, non-determinism, and exceptions, are directly and internally embedded in the logical and computational foundations. We begin by surveying examples where effects reshape logical principles, and then outline three approaches to effectful constructivism, focusing on realizability models: Monadic Combinatory Algebras, which extend classical partial combinatory algebras with effectful computation; Evidenced Frames, a flexible semantic structure capable of uniformly capturing a wide range of effects; and Effectful Higher-Order Logic (EffHOL), a syntactic approach that directly translates logical propositions into specifications for effectful programs. We further illustrate how concrete type theories can internalize effects, via the family of type theories TT^□_C. Together, these works demonstrate that effectful constructivism is not merely possible but a natural and robust extension of traditional frameworks.
Cite as
Liron Cohen. Computation First: Rebuilding Constructivism with Effects (Invited Talk). In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{cohen:LIPIcs.FSCD.2025.1,
author = {Cohen, Liron},
title = {{Computation First: Rebuilding Constructivism with Effects}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {1:1--1:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.1},
URN = {urn:nbn:de:0030-drops-236167},
doi = {10.4230/LIPIcs.FSCD.2025.1},
annote = {Keywords: Effectful constructivism, realizability, type theory, monadic combinatory algebras, evidenced frame}
}
Document
Invited Talk
Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs (Invited Talk)
Abstract
Neuro-symbolic programs, i.e. programs containing both machine learning components and traditional symbolic code, are becoming increasingly widespread. Finding a general methodology for verifying such programs is challenging due to both the number of different tools involved and the intricate interface between the "neural" and "symbolic" program components. In this paper we present a general decomposition of the neuro-symbolic verification problem into parts, and examine the problem of the embedding gap that occurs when one tries to combine proofs about the neural and symbolic components. To address this problem we then introduce Vehicle - standing as an abbreviation for a "verification condition language" - an intermediate programming language interface between machine learning frameworks, automated theorem provers, and dependently-typed formalisations of neuro-symbolic programs. Vehicle allows users to specify the properties of the neural components of neuro-symbolic programs once, and then safely compile the specification to each interface using a tailored typing and compilation procedure. We give a high-level overview of Vehicle’s overall design, its interfaces and compilation & type-checking procedures, and then demonstrate its utility by formally verifying the safety of a simple autonomous car controlled by a neural network, operating in a stochastic environment with imperfect information.
Cite as
Matthew L. Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz, and Luca Arnaboldi. Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs (Invited Talk). In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 2:1-2:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{daggitt_et_al:LIPIcs.FSCD.2025.2,
author = {Daggitt, Matthew L. and Kokke, Wen and Atkey, Robert and Komendantskaya, Ekaterina and Slusarz, Natalia and Arnaboldi, Luca},
title = {{Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {2:1--2:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.2},
URN = {urn:nbn:de:0030-drops-236172},
doi = {10.4230/LIPIcs.FSCD.2025.2},
annote = {Keywords: Neural Network Verification, Types, Interactive Theorem Provers}
}
Document
Invited Talk
Unsolvable Terms in Filter Models (Invited Talk)
Abstract
Intersection type theories (itt’s) and filter models, i.e. λ-calculus models generated by itt’s, are reviewed in full generality. In this framework, which subsumes most λ-calculus models in the literature based on Scott-continuous functions, we discuss the interpretation of unsolvable terms. We give a necessary, but not sufficient, condition on an itt for the interpretation of some unsolvable term to be non-trivial in the filter model it generates. This result is obtained building on a type theoretic characterisation of the fine structure of unsolvables.
Cite as
Mariangiola Dezani-Ciancaglini, Paola Giannini, and Furio Honsell. Unsolvable Terms in Filter Models (Invited Talk). In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 3:1-3:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{dezaniciancaglini_et_al:LIPIcs.FSCD.2025.3,
author = {Dezani-Ciancaglini, Mariangiola and Giannini, Paola and Honsell, Furio},
title = {{Unsolvable Terms in Filter Models}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {3:1--3:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.3},
URN = {urn:nbn:de:0030-drops-236181},
doi = {10.4230/LIPIcs.FSCD.2025.3},
annote = {Keywords: \lambda-calculus, Intersection Types, Unsolvable Terms, Filter Models}
}
Document
Substructural Parametricity
Abstract
Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary logical relations that allow us to prove consequences of parametricity for a range of substructural type systems. A key idea is to parameterize the relation by an algebra, which we exemplify with a monoid and commutative monoid to interpret ordered and linear type systems, respectively. We prove the fundamental theorem of logical relations and apply it to deduce extensional properties of inhabitants of certain types. Examples include demonstrating that the ordered types for list append and reversal are inhabited by exactly one function, as are types of some tree traversals. Similarly, the linear type of the identity function on lists is inhabited only by permutations of the input. Our most advanced example shows that the ordered type of the list fold function is inhabited only by the fold function.
Cite as
C. B. Aberlé, Karl Crary, Chris Martens, and Frank Pfenning. Substructural Parametricity. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{aberle_et_al:LIPIcs.FSCD.2025.4,
author = {Aberl\'{e}, C. B. and Crary, Karl and Martens, Chris and Pfenning, Frank},
title = {{Substructural Parametricity}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {4:1--4:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.4},
URN = {urn:nbn:de:0030-drops-236193},
doi = {10.4230/LIPIcs.FSCD.2025.4},
annote = {Keywords: Substructural type systems, logical relations, ordered logic}
}
Document
The Cost of Skeletal Call-By-Need, Smoothly
Abstract
Skeletal call-by-need is an optimization of call-by-need evaluation also known as "fully lazy sharing": when the duplication of a value has to take place, it is first split into "skeleton", which is then duplicated, and "flesh" which is instead kept shared.
Here, we provide two cost analyses of skeletal call-by-need. Firstly, we provide a family of terms showing that skeletal call-by-need can be asymptotically exponentially faster than call-by-need in both time and space; it is the first such evidence, to our knowledge.
Secondly, we prove that skeletal call-by-need can be implemented efficiently, that is, with bi-linear overhead. This result is obtained by providing a new smooth presentation of ideas by Shivers and Wand for the reconstruction of skeletons, which is then smoothly plugged into the study of an abstract machine following the distillation technique by Accattoli et al.
Cite as
Beniamino Accattoli, Francesco Magliocca, Loïc Peyrot, and Claudio Sacerdoti Coen. The Cost of Skeletal Call-By-Need, Smoothly. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{accattoli_et_al:LIPIcs.FSCD.2025.5,
author = {Accattoli, Beniamino and Magliocca, Francesco and Peyrot, Lo\"{i}c and Sacerdoti Coen, Claudio},
title = {{The Cost of Skeletal Call-By-Need, Smoothly}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {5:1--5:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.5},
URN = {urn:nbn:de:0030-drops-236206},
doi = {10.4230/LIPIcs.FSCD.2025.5},
annote = {Keywords: \lambda-calculus, abstract machines, call-by-need, cost models}
}
Document
Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
Abstract
We present novel semiring semantics for abstract reduction systems (ARSs). More precisely, we provide a weighted version of ARSs, where the reduction steps induce weights from a semiring. Inspired by provenance analysis in database theory and logic, we obtain a formalism that can be used for provenance analysis of arbitrary ARSs. Our semantics handle (possibly unbounded) non-determinism and possibly infinite reductions. Moreover, we develop several techniques to prove upper and lower bounds on the weights resulting from our semantics, and show that in this way one obtains a uniform approach to analyze several different properties like termination, derivational complexity, space complexity, safety, as well as combinations of these properties.
Cite as
Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl, and Joost-Pieter Katoen. Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{ahrens_et_al:LIPIcs.FSCD.2025.6,
author = {Ahrens, Emma and Kassing, Jan-Christoph and Giesl, J\"{u}rgen and Katoen, Joost-Pieter},
title = {{Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {6:1--6:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.6},
URN = {urn:nbn:de:0030-drops-236215},
doi = {10.4230/LIPIcs.FSCD.2025.6},
annote = {Keywords: Rewriting, Semirings, Semantics, Termination, Verification}
}
Document
Combining Generalization Algorithms in Regular Collapse-Free Theories
Abstract
We look at the generalization problem modulo some equational theories. This problem is dual to the unification problem: given two input terms, we want to find a common term whose respective two instances are equivalent to the original terms modulo the theory.
There exist algorithms for finding generalizations over various equational theories. We focus on modular construction of equational generalization algorithms for the union of signature-disjoint theories. Specifically, we consider the class of regular and collapse-free theories, showing how to combine existing generalization algorithms to produce specific solutions in these cases.
Additionally, we identify a class of theories that admit a generalization algorithm based on the application of axioms to resolve the problem. To define this class, we rely on the notion of syntactic theories, a concept originally introduced to develop unification procedures similar to the one known for syntactic unification. We demonstrate that syntactic theories are also helpful in developing generalization procedures similar to those used for syntactic generalization.
Cite as
Mauricio Ayala-Rincón, David M. Cerna, Temur Kutsia, and Christophe Ringeissen. Combining Generalization Algorithms in Regular Collapse-Free Theories. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2025.7,
author = {Ayala-Rinc\'{o}n, Mauricio and Cerna, David M. and Kutsia, Temur and Ringeissen, Christophe},
title = {{Combining Generalization Algorithms in Regular Collapse-Free Theories}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {7:1--7:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.7},
URN = {urn:nbn:de:0030-drops-236228},
doi = {10.4230/LIPIcs.FSCD.2025.7},
annote = {Keywords: Generalization, Anti-unification, Equational theories, Combination}
}
Document
The Unification Type of an Equational Theory May Depend on the Instantiation Preorder
Abstract
The unification type of an equational theory is defined using a preorder on substitutions, called the instantiation preorder, whose scope is either restricted to the variables occurring in the unification problem, or unrestricted such that all variables are considered. It has been known for more than three decades that the unification type of an equational theory may vary, depending on which instantiation preorder is used. More precisely, it was shown in 1991 that the theory ACUI of an associative, commutative, and idempotent binary function symbol with a unit is unitary w.r.t. the restricted instantiation preorder, but not unitary w.r.t. the unrestricted one. In 2016 this result was strengthened by showing that the unrestricted type of this theory also cannot be finitary. Here, we considerably improve on this result by proving that ACUI is infinitary w.r.t. the unrestricted instantiation preorder, thus precluding type zero. We also show that, w.r.t. this preorder, the unification type of ACU (where idempotency is removed from the axioms) and of AC (where additionally the unit is removed) is infinitary, though it is respectively unitary and finitary in the restricted case. In the other direction, we prove (using the example of unification in the description logic EL) that the unification type may actually improve from type zero to infinitary when switching from the restricted instantiation preorder to the unrestricted one. In addition, we establish some general results on the relationship between the two instantiation preorders.
Cite as
Franz Baader and Oliver Fernández Gil. The Unification Type of an Equational Theory May Depend on the Instantiation Preorder. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 8:1-8:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{baader_et_al:LIPIcs.FSCD.2025.8,
author = {Baader, Franz and Fern\'{a}ndez Gil, Oliver},
title = {{The Unification Type of an Equational Theory May Depend on the Instantiation Preorder}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {8:1--8:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.8},
URN = {urn:nbn:de:0030-drops-236230},
doi = {10.4230/LIPIcs.FSCD.2025.8},
annote = {Keywords: Unification type, Instantiation preorder, Equational theories, Modal and Description Logics}
}
Document
A Zoo of Continuity Properties in Constructive Type Theory
Abstract
Continuity principles stating that all functions are continuous play a central role in some schools of constructive mathematics. However, there are different ways to formalise the property of being continuous in constructive foundations. We analyse these continuity properties from the perspective of constructive reverse mathematics. We work in constructive type theory, which can be seen as a minimal foundation for constructive reverse mathematics. We treat continuity of functions F : (Q → A) → R, i.e. with question type Q, answer type A, and result type R. Concretely, we discuss continuity defined via moduli, making the relevant list L : LQ of questions explicit, dialogue trees, making the question-answer process explicit as inductive tree, and tree functions, making the question-answer process explicit as function. We prove equivalences where possible and isolate necessary and sufficient axioms for equivalence proofs. Many of the results we discuss are already present in the works of Hancock, Pattinson, Ghani, Kawai, Fujiwara, Brede, Herbelin, Escardó, and others. Our main contribution is their formulation over a uniform foundation, the observation that no choice axioms are necessary, the generalisation to arbitrary types from natural numbers where possible, and a mechanisation in the Coq/Rocq proof assistant.
Cite as
Martin Baillon, Yannick Forster, Assia Mahboubi, Pierre-Marie Pédrot, and Matthieu Piquerez. A Zoo of Continuity Properties in Constructive Type Theory. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{baillon_et_al:LIPIcs.FSCD.2025.9,
author = {Baillon, Martin and Forster, Yannick and Mahboubi, Assia and P\'{e}drot, Pierre-Marie and Piquerez, Matthieu},
title = {{A Zoo of Continuity Properties in Constructive Type Theory}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {9:1--9:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.9},
URN = {urn:nbn:de:0030-drops-236245},
doi = {10.4230/LIPIcs.FSCD.2025.9},
annote = {Keywords: type theory, constructive mathematics, continuity, Coq}
}
Document
Categorical Continuation Semantics for Concurrency
Abstract
Continuation semantics for simple programming languages can be axiomatized as a dialogue category: a symmetric monoidal category equipped with a negation operation. This axiomatization makes clear the relationship between game semantics, CPS transformations, and continuation monads.
In this paper we extend dialogue categories with 2-categorical structure and concurrent primitives. This is inspired by a recent analysis of concurrency based on 2-categorical monads. We show that the fine-grained structure of dialogue categories, not generally available in other semantic models, can be exploited to give a type to concurrent primitives join and fork. Our main theorem is that this simple axiomatization induces a concurrent continuation 2-monad. We also show that this framework is expressive beyond call-by-value monadic programming.
The definitions in this paper are illustrated by concrete constructions in concurrent game semantics, and our results give a formal categorical basis for concurrent strategies. From a more practical perspective, our approach suggests a candidate target language for linear CPS transformations of concurrent programming languages.
Cite as
Flavien Breuvart and Hugo Paquet. Categorical Continuation Semantics for Concurrency. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{breuvart_et_al:LIPIcs.FSCD.2025.10,
author = {Breuvart, Flavien and Paquet, Hugo},
title = {{Categorical Continuation Semantics for Concurrency}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {10:1--10:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.10},
URN = {urn:nbn:de:0030-drops-236251},
doi = {10.4230/LIPIcs.FSCD.2025.10},
annote = {Keywords: denotational semantics, 2-categories, concurrency, continuations, game semantics}
}
Document
Impredicative Encodings of Inductive and Coinductive Types
Abstract
In impredicative type theory (System F, also known as λ2), it is possible to define inductive data types, such as natural numbers and lists. It is also possible to define coinductive data types such as streams. They work well in the sense that their (co)recursion principles obey the expected computation rules (the β-rules). Unfortunately, they do not yield a (co)induction principle [Herman Geuvers, 2001; Ivar Rummelhoff, 2004], because the necessary uniqueness principles are missing (the η-rules). Awodey, Frey, and Speight [Steve Awodey et al., 2018] used an extension of the Calculus of Constructions [Thierry Coquand and Gérard P. Huet, 1988] (λ C) with Σ-types, identity-types, and functional extensionality to define System F style inductive types with an induction principle, by encoding them as a well-chosen subtype, making them initial algebras.
In this paper, we extend their results to coinductive data types, and we detail the example of the stream data type with the desired coinduction principle (also called bisimulation). To do that, we first define quotient types (with the desired η-rules) and we also need a stronger form of the definable existential types. We also show that we can use the original method by Awodey, Frey and Speight for general inductive types by defining W-types with an induction principle. The dual approach for streams can be extended to M-types, the generic notion of coinductive types, and the dual of W-types.
Cite as
Steven Bronsveld, Herman Geuvers, and Niels van der Weide. Impredicative Encodings of Inductive and Coinductive Types. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{bronsveld_et_al:LIPIcs.FSCD.2025.11,
author = {Bronsveld, Steven and Geuvers, Herman and van der Weide, Niels},
title = {{Impredicative Encodings of Inductive and Coinductive Types}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {11:1--11:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.11},
URN = {urn:nbn:de:0030-drops-236263},
doi = {10.4230/LIPIcs.FSCD.2025.11},
annote = {Keywords: Formulas-as-types, impredicativity, inductive types, coinductive types}
}
Document
Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten!
Abstract
Although the λI-calculus is a natural fragment of the λ-calculus, obtained by forbidding the erasure, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable λI-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the λI-calculus, induced by a notion of evaluation trees that we call "Ohana trees". The Ohana tree of a λI-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches.
We develop the associated theories of program approximation: the first approach - more classic - is based on finite trees and continuity, the second adapts Ehrhard and Regnier’s Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a λI-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application. We conclude by discussing the cases of Lévy-Longo and Berarducci trees, and generalizations to the full λ-calculus.
Cite as
Rémy Cerda, Giulio Manzonetto, and Alexis Saurin. Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten!. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{cerda_et_al:LIPIcs.FSCD.2025.12,
author = {Cerda, R\'{e}my and Manzonetto, Giulio and Saurin, Alexis},
title = {{Ohana Trees and Taylor Expansion for the \lambdaI-Calculus: No variable gets left behind or forgotten!}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {12:1--12:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.12},
URN = {urn:nbn:de:0030-drops-236277},
doi = {10.4230/LIPIcs.FSCD.2025.12},
annote = {Keywords: \lambda-calculus, program approximation, Taylor expansion, \lambdaI-calculus, persistent free variables, B\"{o}hm trees, Ohana trees}
}
Document
Unifying Boolean and Algebraic Descriptive Complexity
Abstract
We introduce ultrarings, which simultaneously generalize commutative rings and Boolean lextensive categories. As such, they allow to blend together standard algebraic notions (from commutative algebra) and logical notions (from categorical logic), providing a unifying descriptive framework in which complexity classes over arbitrary rings (as in the Blum, Schub, Smale model) and usual, Boolean complexity classes may be captured in a uniform way.
Cite as
Baptiste Chanus, Damiano Mazza, and Morgan Rogers. Unifying Boolean and Algebraic Descriptive Complexity. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{chanus_et_al:LIPIcs.FSCD.2025.13,
author = {Chanus, Baptiste and Mazza, Damiano and Rogers, Morgan},
title = {{Unifying Boolean and Algebraic Descriptive Complexity}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {13:1--13:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.13},
URN = {urn:nbn:de:0030-drops-236286},
doi = {10.4230/LIPIcs.FSCD.2025.13},
annote = {Keywords: Descriptive complexity theory, Categorical logic, Blum-Shub-Smale complexity}
}
Document
From Partial to Monadic: Combinatory Algebra with Effects
Abstract
Partial Combinatory Algebras (PCAs) provide a foundational model of the untyped λ-calculus and serve as the basis for many notions of computability, such as realizability theory. However, PCAs support a very limited notion of computation by only incorporating non-termination as a computational effect. To provide a framework that better internalizes a wide range of computational effects, this paper puts forward the notion of Monadic Combinatory Algebras (MCAs). MCAs generalize the notion of PCAs by structuring the combinatory algebra over an underlying computational effect, embodied by a monad. We show that MCAs can support various side effects through the underlying monad, such as non-determinism, stateful computation and continuations. We further obtain a categorical characterization of MCAs within Freyd Categories, following a similar connection for PCAs. Moreover, we explore the application of MCAs in realizability theory, presenting constructions of effectful realizability triposes and assemblies derived through evidenced frames, thereby generalizing traditional PCA-based realizability semantics. The monadic generalization of the foundational notion of PCAs provides a comprehensive and powerful framework for internally reasoning about effectful computations, paving the path to a more encompassing study of computation and its relationship with realizability models and programming languages.
Cite as
Liron Cohen, Ariel Grunfeld, Dominik Kirst, and Étienne Miquey. From Partial to Monadic: Combinatory Algebra with Effects. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 14:1-14:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{cohen_et_al:LIPIcs.FSCD.2025.14,
author = {Cohen, Liron and Grunfeld, Ariel and Kirst, Dominik and Miquey, \'{E}tienne},
title = {{From Partial to Monadic: Combinatory Algebra with Effects}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {14:1--14:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.14},
URN = {urn:nbn:de:0030-drops-236297},
doi = {10.4230/LIPIcs.FSCD.2025.14},
annote = {Keywords: Combinatory algebras, Monads, Effects, Realizability, Evidenced frames}
}
Document
On the Metric Nature of (Differential) Logical Relations
Abstract
Differential logical relations are a method to measure distances between higher-order programs. They differ from standard methods based on program metrics in that differences between functional programs are themselves functions, relating errors in input with errors in output, this way providing a more fine grained, contextual, information. The aim of this paper is to clarify the metric nature of differential logical relations. While previous work has shown that these do not give rise, in general, to (quasi-)metric spaces nor to partial metric spaces, we show that the distance functions arising from such relations, that we call quasi-quasi-metrics, can be related to both quasi-metrics and partial metrics, the latter being also captured by suitable relational definitions. Moreover, we exploit such connections to deduce some new compositional reasoning principles for program differences.
Cite as
Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone. On the Metric Nature of (Differential) Logical Relations. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 15:1-15:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{dallago_et_al:LIPIcs.FSCD.2025.15,
author = {Dal Lago, Ugo and Hoshino, Naohiko and Pistone, Paolo},
title = {{On the Metric Nature of (Differential) Logical Relations}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {15:1--15:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.15},
URN = {urn:nbn:de:0030-drops-236300},
doi = {10.4230/LIPIcs.FSCD.2025.15},
annote = {Keywords: Differential Logical Relations, Quantales, Quasi-Metrics, Partial Metrics}
}
Document
Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic
Abstract
We revisit sequentialization proofs associated with the Danos-Regnier correctness criterion in the theory of proof nets of linear logic. Our approach relies on a generalization of Yeo’s theorem for graphs, based on colorings of half-edges. This happens to be the appropriate level of abstraction to extract sequentiality information from a proof net without modifying its graph structure. We thus obtain different ways of recovering a sequent calculus derivation from a proof net inductively, by relying on a splitting ⅋-vertex, on a splitting ⊗-vertex, on a splitting terminal vertex, etc.
The proof of our Yeo-style theorem relies on a key lemma that we call cusp minimization. Given a coloring of half-edges, a cusp in a path is a vertex whose adjacent half-edges in the path have the same color. And, given a cycle with at least one cusp and subject to suitable hypotheses, cusp minimization constructs a cycle with strictly less cusps. In the absence of cusp-free cycles, cusp minimization is then enough to ensure the existence of a splitting vertex, i.e. a vertex that is a cusp of any cycle it belongs to. Our theorem subsumes several graph-theoretical results, including some known to be equivalent to Yeo’s theorem. The novelty is that they can be derived in a straightforward way, just by defining a dedicated coloring, again without any modification of the underlying graph structure (vertices and edges) - similar results from the literature required more involved encodings.
Cite as
Rémi Di Guardia, Olivier Laurent, Lorenzo Tortora de Falco, and Lionel Vaux Auclair. Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{diguardia_et_al:LIPIcs.FSCD.2025.16,
author = {Di Guardia, R\'{e}mi and Laurent, Olivier and Tortora de Falco, Lorenzo and Vaux Auclair, Lionel},
title = {{Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {16:1--16:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.16},
URN = {urn:nbn:de:0030-drops-236317},
doi = {10.4230/LIPIcs.FSCD.2025.16},
annote = {Keywords: Linear Logic, Proof Net, Sequentialization, Graph Theory, Yeo’s Theorem}
}
Document
Mechanized Undecidability of Higher-Order Beta-Matching
Abstract
Higher-order β-matching is the following decision problem: given two simply typed λ-terms, can the first term be instantiated to be β-equivalent to the second term? This problem was formulated by Huet in the 1970s and shown undecidable by Loader in 2003 by reduction from λ-definability.
The present work provides a novel undecidability proof for higher-order β-matching, in an effort to verify this result by means of a proof assistant. Rather than starting from λ-definability, the presented proof encodes a restricted form of string rewriting as higher-order β-matching. The particular approach is similar to Urzyczyn’s undecidability result for intersection type inhabitation.
The presented approach has several advantages. First, the proof is simpler to verify in full detail due to the simple form of rewriting systems, which serve as a starting point. Second, undecidability of the considered problem in string rewriting is already certified using the Coq proof assistant. As a consequence, we obtain a certified many-one reduction from the Halting Problem to higher-order β-matching. Third, the presented approach identifies a uniform construction which shows undecidability of higher-order β-matching, λ-definability, and intersection type inhabitation.
The presented undecidability proof is mechanized in the Coq proof assistant and contributed to the existing Coq Library of Undecidability Proofs.
Cite as
Andrej Dudenhefner. Mechanized Undecidability of Higher-Order Beta-Matching. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 17:1-17:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{dudenhefner:LIPIcs.FSCD.2025.17,
author = {Dudenhefner, Andrej},
title = {{Mechanized Undecidability of Higher-Order Beta-Matching}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {17:1--17:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.17},
URN = {urn:nbn:de:0030-drops-236323},
doi = {10.4230/LIPIcs.FSCD.2025.17},
annote = {Keywords: lambda-calculus, simple types, undecidability, higher-order matching, mechanization, Coq}
}
Document
Knowledge Problems vs Unification and Matching: Dichotomy Results
Abstract
The research area of cryptographic protocol analysis contains a number of innovative algorithms and procedures for checking various security properties of protocols. Most of these procedures focus on solving one of several "knowledge problems" that model intruder knowledge. Solving these problems can demonstrate the ability of the intruder to obtain some forbidden information of the protocol, such as secret keys. Two important examples of these problems are the deduction problem and the static equivalence problem.
Deduction is concerned with the ability to derive a term from a set of terms (or knowledge) obtained from the observation of a protocol instance. Static equivalence, on the other hand, is concerned with distinguishing between two runs of a protocol based on two sets of knowledge. These two knowledge problems at first inspection appear to be very close to the older automated reasoning problems of matching and unification. However, this first impression is wrong, and there have been a few results that have shown theories where one problem, such as unification, is undecidable but another problem, such as deduction, is decidable. These existing dichotomy results were, however, incomplete, and not all cases had been examined, thus leaving the possibility of some connection between the problems for those unexamined cases.
In this paper, we consider the missing dichotomy cases. For each of the remaining cases, we demonstrate a theory that separates the two problems. In addition, once the dichotomy results are completed, it leaves open the question of the existence of non-trivial classes of theories for which all four of the problems are decidable. One example for which this is true is the well-known class of subterm convergent term rewrite systems. In this paper, we develop another example, a class of restrictive permutative theories for which all problems are likewise decidable.
Cite as
Serdar Erbatur, Andrew M. Marshall, Paliath Narendran, and Christophe Ringeissen. Knowledge Problems vs Unification and Matching: Dichotomy Results. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{erbatur_et_al:LIPIcs.FSCD.2025.18,
author = {Erbatur, Serdar and Marshall, Andrew M. and Narendran, Paliath and Ringeissen, Christophe},
title = {{Knowledge Problems vs Unification and Matching: Dichotomy Results}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {18:1--18:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.18},
URN = {urn:nbn:de:0030-drops-236331},
doi = {10.4230/LIPIcs.FSCD.2025.18},
annote = {Keywords: Knowledge Problems, Unification, Matching, Decidability}
}
Document
Internal Effectful Forcing in System T
Abstract
The effectful forcing technique allows one to show that the denotation of a closed System T term of type (ι ⇒ ι) ⇒ ι in the set-theoretical model is a continuous function (ℕ → ℕ) → ℕ. For this purpose, an alternative dialogue-tree semantics is defined and related to the set-theoretical semantics by a logical relation. In this paper, we apply effectful forcing to show that the dialogue tree of a System T term is itself System T-definable, using the Church encoding of trees.
Cite as
Martín H. Escardó, Bruno da Rocha Paiva, Vincent Rahli, and Ayberk Tosun. Internal Effectful Forcing in System T. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{escardo_et_al:LIPIcs.FSCD.2025.19,
author = {Escard\'{o}, Mart{\'\i}n H. and da Rocha Paiva, Bruno and Rahli, Vincent and Tosun, Ayberk},
title = {{Internal Effectful Forcing in System T}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {19:1--19:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.19},
URN = {urn:nbn:de:0030-drops-236344},
doi = {10.4230/LIPIcs.FSCD.2025.19},
annote = {Keywords: Effectful forcing, Continuity, System T, Constructive Mathematics}
}
Document
An Innermost DP Framework for Constrained Higher-Order Rewriting
Abstract
Logically constrained simply-typed term rewriting systems (LCSTRSs) are a higher-order formalism for program analysis with support for primitive data types. The termination problem of LCSTRSs has been studied so far in the setting of full rewriting. This paper modifies the higher-order constrained dependency pair framework to prove innermost termination, which corresponds to the termination of programs under call by value. We also show that the notion of universal computability with respect to innermost rewriting can be effectively handled in the modified, innermost framework, which lays the foundation for open-world termination analysis of programs under call by value via LCSTRSs.
Cite as
Carsten Fuhs, Liye Guo, and Cynthia Kop. An Innermost DP Framework for Constrained Higher-Order Rewriting. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 20:1-20:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{fuhs_et_al:LIPIcs.FSCD.2025.20,
author = {Fuhs, Carsten and Guo, Liye and Kop, Cynthia},
title = {{An Innermost DP Framework for Constrained Higher-Order Rewriting}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {20:1--20:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.20},
URN = {urn:nbn:de:0030-drops-236359},
doi = {10.4230/LIPIcs.FSCD.2025.20},
annote = {Keywords: Higher-order term rewriting, constrained rewriting, innermost termination, call by value, open-world analysis, dependency pairs}
}
Document
An Expressive Trace Logic for Recursive Programs
Abstract
We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed points, for precise specification of programs with recursive procedures. Both programs and trace formulas are equipped with a direct-style, fully compositional, denotational semantics that on programs coincides with the standard SOS of recursive programs. We design a compositional proof calculus for proving finite-trace program properties, and prove soundness as well as (relative) completeness. We show that each program can be mapped to a semantics-preserving trace formula and, vice versa, each trace formula can be mapped to a canonical program over slightly extended programs, resulting in a Galois connection between programs and formulas. Our results shed light on the correspondence between programming constructs and logical connectives.
Cite as
Dilian Gurov and Reiner Hähnle. An Expressive Trace Logic for Recursive Programs. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{gurov_et_al:LIPIcs.FSCD.2025.21,
author = {Gurov, Dilian and H\"{a}hnle, Reiner},
title = {{An Expressive Trace Logic for Recursive Programs}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {21:1--21:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.21},
URN = {urn:nbn:de:0030-drops-236360},
doi = {10.4230/LIPIcs.FSCD.2025.21},
annote = {Keywords: Denotational semantics, compositional semantics, program specification, compositional verification, fixed point logic, trace logic}
}
Document
Branch Sequentialization in Quantum Polytime
Abstract
Quantum algorithms leverage the use of quantumly-controlled data in order to achieve computational advantage. This implies that the programs use constructs depending on quantum data and not just classical data such as measurement outcomes. Current compilation strategies for quantum control flow involve compiling the branches of a quantum conditional, either in-depth or in-width, which in general leads to circuits of exponential size. This problem is coined as the branch sequentialization problem. We introduce and study a compilation technique for avoiding branch sequentialization on a language that is sound and complete for quantum polynomial time, thus, improving on existing polynomial-size-preserving compilation techniques.
Cite as
Emmanuel Hainry, Romain Péchoux, and Mário Silva. Branch Sequentialization in Quantum Polytime. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{hainry_et_al:LIPIcs.FSCD.2025.22,
author = {Hainry, Emmanuel and P\'{e}choux, Romain and Silva, M\'{a}rio},
title = {{Branch Sequentialization in Quantum Polytime}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {22:1--22:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.22},
URN = {urn:nbn:de:0030-drops-236373},
doi = {10.4230/LIPIcs.FSCD.2025.22},
annote = {Keywords: Quantum Programs, Implicit Computational Complexity, Quantum Circuits}
}
Document
∞-Categorical Models of Linear Logic
Abstract
The notion of categorical model of linear logic is now well studied and established around the notion of linear-non-linear adjunction, which encompasses the earlier notions of Seely categories, Lafont categories and linear categories. These categorical structures have counterparts in the realm of ∞-categories, which can thus be thought of as weak forms of models of linear logic. The goal of this article is to formally introduce them and study their relationships. We show that ∞-linear-non-linear adjunctions still play the role of a unifying notion of model in this setting. Moreover, we provide a sufficient condition for a symmetric monoidal ∞-category to be Lafont. Finally, we illustrate our constructions by providing models: we construct linear-non-linear adjunctions that generalize well-known models in relations (and variants based on profunctors or spans), domains and vector spaces. In particular, we introduce a model based on spectra, a homotopical variant of abelian groups.
Cite as
Eliès Harington and Samuel Mimram. ∞-Categorical Models of Linear Logic. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 23:1-23:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{harington_et_al:LIPIcs.FSCD.2025.23,
author = {Harington, Eli\`{e}s and Mimram, Samuel},
title = {{∞-Categorical Models of Linear Logic}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {23:1--23:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.23},
URN = {urn:nbn:de:0030-drops-236381},
doi = {10.4230/LIPIcs.FSCD.2025.23},
annote = {Keywords: linear logic, linear-non-linear adjunction, ∞-category, spectrum}
}
Document
Quantitative Types for the Functional Machine Calculus
Abstract
The Functional Machine Calculus (FMC, Heijltjes 2022) extends the lambda-calculus with the computational effects of global mutable store, input/output, and probabilistic choice while maintaining confluent reduction and simply-typed strong normalization. Based in a simple call-by-name stack machine in the style of Krivine, the FMC models effects through additional argument stacks, and introduces sequential composition through a continuation stack to encode call-by-value behaviour, where simple types guarantee termination of the machine.
The present paper provides a discipline of quantitative types, also known as non-idempotent intersection types, for the FMC, in two variants. In the weak variant, typeability coincides with termination of the stack machine and with spine normalization, while exactly measuring the transitions in machine evaluation. The strong variant characterizes strong normalization through a notion of perpetual evaluation, while giving an upper bound to the length of reductions. Through the encoding of effects, quantitative typeability coincides with termination for higher-order mutable store, input/output, and probabilistic choice.
Cite as
Willem Heijltjes. Quantitative Types for the Functional Machine Calculus. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 24:1-24:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{heijltjes:LIPIcs.FSCD.2025.24,
author = {Heijltjes, Willem},
title = {{Quantitative Types for the Functional Machine Calculus}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {24:1--24:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.24},
URN = {urn:nbn:de:0030-drops-236391},
doi = {10.4230/LIPIcs.FSCD.2025.24},
annote = {Keywords: lambda-calculus, computational effects, intersection types}
}
Document
Completeness of the Decreasing Diagrams Method for Proving Confluence of Rewriting Systems of the Least Uncountable Cardinality
Abstract
We show that every confluent abstract rewriting system (ARS) of the cardinality that does not exceed the first uncountable cardinal belongs to the class DCR₃, i.e. the class of confluent ARS for which confluence can be proved with the the help of the decreasing diagrams method using the set of labels {0,1,2} ordered in such a way that 0<1<2 (in the general case, the decreasing diagrams method with two labels is not sufficient for proving confluence of such ARS). Under the Continuum Hypothesis this result implies that the decreasing diagrams method is sufficient for establishing confluence of ARS on many structures of interest to applied mathematics and various interdisciplinary fields (confluence of ARS on real numbers, continuous real functions, etc.).
We provide a machine-checked formal proof of a formalized version of the main result in Isabelle proof assistant using HOL logic and the HOL-Cardinals theory. An extended version of this formalization is available in the Archive of Formal Proofs.
Cite as
Ievgen Ivanov. Completeness of the Decreasing Diagrams Method for Proving Confluence of Rewriting Systems of the Least Uncountable Cardinality. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{ivanov:LIPIcs.FSCD.2025.25,
author = {Ivanov, Ievgen},
title = {{Completeness of the Decreasing Diagrams Method for Proving Confluence of Rewriting Systems of the Least Uncountable Cardinality}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {25:1--25:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.25},
URN = {urn:nbn:de:0030-drops-236404},
doi = {10.4230/LIPIcs.FSCD.2025.25},
annote = {Keywords: confluence, decreasing diagrams method, rewriting systems, reduction, formal methods, formal proofs, formal verification, non-discrete models, nondeterministic models, interval models}
}
Document
Functorial Models of Differential Linear Logic
Abstract
Differentiation in logic has several sources of inspiration. The most recent is differentiable programming, models of which demand functoriality and good typing properties. More historical is reverse denotational semantics, taking inspiration from models of Linear Logic to differentiate proofs and λ-terms. In this paper, we take advantage of the rich structure of categorical models of Linear Logic to give a new functorial presentation of differentiation. We define differentiation as a functor from a coslice of the category of smooth maps to the category of linear maps. Extending linear-non-linear adjunction models of Linear Logic, this produces models of Differential Linear Logic. We use these functorial presentations to shed new light on integration in differential categories.
Cite as
Marie Kerjean, Valentin Maestracci, and Morgan Rogers. Functorial Models of Differential Linear Logic. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 26:1-26:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{kerjean_et_al:LIPIcs.FSCD.2025.26,
author = {Kerjean, Marie and Maestracci, Valentin and Rogers, Morgan},
title = {{Functorial Models of Differential Linear Logic}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {26:1--26:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.26},
URN = {urn:nbn:de:0030-drops-236419},
doi = {10.4230/LIPIcs.FSCD.2025.26},
annote = {Keywords: Categorical semantics, Differential Programming, Linear Logic}
}
Document
What Does It Take to Certify a Conversion Checker?
Abstract
We report on a detailed exploration of the properties of conversion (definitional equality) in dependent type theory, with the goal of certifying decision procedures for it. While in that context the property of normalisation has attracted the most light, we instead emphasize the importance of injectivity properties, showing that they alone are both crucial and sufficient to certify most desirable properties of conversion checkers. We also explore the certification of a fully untyped conversion checker, with respect to a typed specification, and show that the story is mostly unchanged, although the exact injectivity properties needed are subtly different.
Cite as
Meven Lennon-Bertrand. What Does It Take to Certify a Conversion Checker?. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{lennonbertrand:LIPIcs.FSCD.2025.27,
author = {Lennon-Bertrand, Meven},
title = {{What Does It Take to Certify a Conversion Checker?}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {27:1--27:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.27},
URN = {urn:nbn:de:0030-drops-236428},
doi = {10.4230/LIPIcs.FSCD.2025.27},
annote = {Keywords: Dependent types, Bidirectional typing, Certified software}
}
Document
Grading Call-By-Push-Value, Explicitly and Implicitly
Abstract
We present call-by-push-value with effects (CBPVE), a refinement of Levy’s call-by-push-value (CBPV) calculus in which the types contain behavioural information about the effects of computations. CBPVE fits well into the existing literature on graded types and computational effects. We demonstrate this by providing graded call-by-value and call-by-name translations into CBPVE, and a semantics based on algebras for a graded monad.
CBPVE is designed as a standalone calculus, with explicit grade information in the syntax. We use it to study the assignment of graded types to the terms of an ungraded calculus such as CBPV, essentially treating the grades as implicit. To interpret such terms in a model that accounts for the grades, one has to prove a coherence result for the implicit grades. We show that, in the case of a graded monadic semantics, the necessary coherence result is false in general. To solve this problem, we show that a mild condition on the algebra of grades is enough to guarantee coherence, giving the first proof of a coherence result for grading, and hence also the first graded monadic semantics for CBPV computations.
Cite as
Dylan McDermott. Grading Call-By-Push-Value, Explicitly and Implicitly. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{mcdermott:LIPIcs.FSCD.2025.28,
author = {McDermott, Dylan},
title = {{Grading Call-By-Push-Value, Explicitly and Implicitly}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {28:1--28:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.28},
URN = {urn:nbn:de:0030-drops-236432},
doi = {10.4230/LIPIcs.FSCD.2025.28},
annote = {Keywords: computational effect, effect system, call-by-push-value, graded monad}
}
Document
Linear Logic Using Negative Connectives
Abstract
In linear logic, the invertibility of a connective’s right-introduction rule is equivalent to the non-invertibility of its left-introduction rule. This duality motivates the concept of polarity: a connective is termed negative if its right-introduction rule is invertible, and positive otherwise. A two-sided sequent calculus for first-order linear logic featuring only negative connectives exhibits a compelling proof theory. Proof search in such a system unfolds through alternating phases of invertible (right-introduction) rules and non-invertible (left-introduction) rules, mirroring the processes of goal-reduction and backchaining, respectively. These phases are formalized here using the framework of multifocused proofs. We analyze linear logic by dissecting it into three sublogics: L₀ (first-order intuitionistic logic with conjunction, implication, and universal quantification); L₁ (an extension of L₀ incorporating linear implication which preserves its intuitionistic nature); and L₂ (which includes multiplicative falsity ⊥ and encompasses classical linear logic). It is worth noting that the single-conclusion restriction on sequents, a constraint imposed by Gentzen, is not a prerequisite for defining intuitionistic logic proofs within this framework, as it emerges naturally by restricting the formulas to those of L₀ and L₁. While multifocused proofs of L₂ sequents can accommodate parallel applications of left-introduction rules, proofs of L₀ and L₁ sequents cannot leverage such parallel rule applications. This notion of parallelism within proofs enables a novel approach to handling disjunctions and existential quantifiers in the natural deduction system for intuitionistic logic.
Cite as
Dale Miller. Linear Logic Using Negative Connectives. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 29:1-29:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{miller:LIPIcs.FSCD.2025.29,
author = {Miller, Dale},
title = {{Linear Logic Using Negative Connectives}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {29:1--29:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.29},
URN = {urn:nbn:de:0030-drops-236442},
doi = {10.4230/LIPIcs.FSCD.2025.29},
annote = {Keywords: Linear logic, multifocused proofs, sequent calculus}
}
Document
Coherent Tietze Transformations of 1-Polygraphs in Homotopy Type Theory
Abstract
Polygraphs play a fundamental role in algebra, geometry, and computer science, by generalizing group presentations to higher-dimensional structures and encoding coherence for those. They have recently been adapted by Kraus and von Raumer to the setting of homotopy type theory, where they are useful to define and study higher inductive types. Here, we develop the theory of 1-dimensional polygraphs, which correspond to presentations of sets in homotopy type theory. This requires us to introduce a dedicated notion of Tietze transformation, generalizing their well-known counterpart in group theory: the equivalence generated by those transformations characterizes situations where two 1-polygraphs present the same set. We also show a homotopy transfer theorem, which provides a way to transport coherence structures from one 1-polygraph to another. This work lays the foundations for a general theory of polygraphs in arbitrary dimensions, which should be useful for instance to define and study coherent group presentations, allowing for synthetic (co)homology computations. Most of the results in the article have been formalized with the Agda proof assistant using the cubical HoTT library.
Cite as
Samuel Mimram and Émile Oleon. Coherent Tietze Transformations of 1-Polygraphs in Homotopy Type Theory. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{mimram_et_al:LIPIcs.FSCD.2025.30,
author = {Mimram, Samuel and Oleon, \'{E}mile},
title = {{Coherent Tietze Transformations of 1-Polygraphs in Homotopy Type Theory}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {30:1--30:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.30},
URN = {urn:nbn:de:0030-drops-236456},
doi = {10.4230/LIPIcs.FSCD.2025.30},
annote = {Keywords: homotopy type theory, polygraph, Tietze transformation, coherence}
}
Document
Higher-Dimensional Automata: Extension to Infinite Tracks
Abstract
We introduce higher-dimensional automata for infinite interval ipomsets (ω-HDAs). We define key concepts from different points of view, inspired from their finite counterparts. Then we explore languages recognized by ω-HDAs under Büchi and Muller semantics. We show that Muller acceptance is more expressive than Büchi acceptance and, in contrast to the finite case, both semantics do not yield languages closed under subsumption. Then, we adapt the original rational operations to deal with ω-HDAs and show that while languages of ω-HDAs are ω-rational, not all ω-rational languages can be expressed by ω-HDAs.
Cite as
Luc Passemard, Amazigh Amrane, and Uli Fahrenberg. Higher-Dimensional Automata: Extension to Infinite Tracks. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 31:1-31:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{passemard_et_al:LIPIcs.FSCD.2025.31,
author = {Passemard, Luc and Amrane, Amazigh and Fahrenberg, Uli},
title = {{Higher-Dimensional Automata: Extension to Infinite Tracks}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {31:1--31:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.31},
URN = {urn:nbn:de:0030-drops-236466},
doi = {10.4230/LIPIcs.FSCD.2025.31},
annote = {Keywords: Higher-dimensional automata, concurrency theory, omega pomsets, B\"{u}chi acceptance, Muller acceptance, interval pomsets, pomsets with interfaces}
}
Document
Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation
Abstract
Analyzing Maehara’s method for proving Craig’s interpolation theorem, we extract a "proof relevant" interpolation theorem for first-order LL in the sense that if π is a cut-free sequent proof of A⊢ B, we can find a formula C in the common vocabulary of A and B and proofs π₁,π₂ of A⊢ C and C⊢ B respectively such that π₁ composed with π₂ cut-reduces to π. As a direct corollary, we get similar proof relevant interpolation results for LJ and LK using linear translations. This refined interpolation is then rephrased in terms of a cut-introduction process synthetizing the interpolant.
Finally, we analyze the computational content of interpolation by proving an interpolation result for Curien and Herbelin’s Duality of Computation.
Cite as
Alexis Saurin. Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 32:1-32:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{saurin:LIPIcs.FSCD.2025.32,
author = {Saurin, Alexis},
title = {{Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {32:1--32:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.32},
URN = {urn:nbn:de:0030-drops-236478},
doi = {10.4230/LIPIcs.FSCD.2025.32},
annote = {Keywords: Classical Logic, Interpolation, Cut Elimination, Linear Logic, Sequent calculus, System L}
}
Document
Solving Guarded Domain Equations in Presheaves over Ordinals and Mechanizing It
Abstract
Constructing solutions to recursive domain equations is a well-known, important problem in the study of programs and programming languages. Mathematically speaking, the problem is finding a fixed point (up to isomorphism) of a suitable functor over a suitable category. A particularly useful instance, inspired by the step-indexing technique, is where the functor is over (a subcategory of) the category of presheaves over the ordinal ω and the functors are locally-contractive, also known as guarded functors. This corresponds to step-indexing over natural numbers. However, for certain problems, e.g., when dealing with infinite non-determinism, one needs to employ trans-finite step-indexing, i.e., consider presheaf categories over higher ordinals. Prior work on trans-finite step-indexing either only considers a very narrow class of functors over a particularly restricted subcategory of presheaves over higher ordinals, or treats the problem very generally working with sheaves over an arbitrary complete Heyting algebra with a well-founded basis.
In this paper we present a solution to the guarded domain equations problem over all guarded functors over the category of presheaves over ordinal numbers, as well as its mechanization in the Rocq Prover. As the categories of sheaves and presheaves over ordinals are equivalent, our main contribution is simplifying prior work from the setting of the category of sheaves to the setting of the category of presheaves and mechanizing it - presheaves are more amenable to mechanization in a proof assistant.
Cite as
Sergei Stepanenko and Amin Timany. Solving Guarded Domain Equations in Presheaves over Ordinals and Mechanizing It. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 33:1-33:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{stepanenko_et_al:LIPIcs.FSCD.2025.33,
author = {Stepanenko, Sergei and Timany, Amin},
title = {{Solving Guarded Domain Equations in Presheaves over Ordinals and Mechanizing It}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {33:1--33:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.33},
URN = {urn:nbn:de:0030-drops-236486},
doi = {10.4230/LIPIcs.FSCD.2025.33},
annote = {Keywords: Domain Equations, Guarded Fixed Points, Fixed Points, Category Theory, Rocq, Presheaves, Ordinals}
}
Document
Monad Translations for Higher-Order Logic
Abstract
Classical logic can be embedded into intuitionistic logic by inserting double negations in formulas. Several translations generalize this idea by using monad operators instead of double negations. They eliminate particular axioms, for instance the principle of excluded middle or the principle of explosion, and therefore can be used to embed classical logic into intuitionistic logic or intuitionistic logic into minimal logic. Such translations have been defined for first-order logic.
In this paper, we define a translation, parameterized by monad operators, for higher-order logic. In particular, the property that any formula and its translation are equivalent in the presence of the eliminated axiom holds under functional extensionality and propositional extensionality. We apply this translation to embed higher-order classical (respectively intuitionistic) logic into higher-order intuitionistic (respectively minimal) logic. By adapting Friedman’s trick, we show that coherent formulas correspond to a constructive fragment of higher-order classical logic, meaning that we can transform classical proofs into intuitionistic proofs without modifying the proven statements.
Cite as
Thomas Traversié. Monad Translations for Higher-Order Logic. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 34:1-34:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{traversie:LIPIcs.FSCD.2025.34,
author = {Traversi\'{e}, Thomas},
title = {{Monad Translations for Higher-Order Logic}},
booktitle = {10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
pages = {34:1--34:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-374-4},
ISSN = {1868-8969},
year = {2025},
volume = {337},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.34},
URN = {urn:nbn:de:0030-drops-236495},
doi = {10.4230/LIPIcs.FSCD.2025.34},
annote = {Keywords: Higher-order logic, Intuitionistic logic, Kuroda’s translation, Monad}
}