Volume
LIPIcs, Volume 378
11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD)
Event
Editor
Publication Details
- published at: 2026-07-15
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-433-8
Access Numbers
- Detailed Access Statistics available here
-
Total Accesses (updated on a weekly basis)
0Documents
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 378, FSCD 2026, Complete Volume
Abstract
LIPIcs, Volume 378, FSCD 2026, Complete Volume
Cite as
11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 1-716, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Proceedings{pfenning:LIPIcs.FSCD.2026,
title = {{LIPIcs, Volume 378, FSCD 2026, Complete Volume}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {1--716},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026},
URN = {urn:nbn:de:0030-drops-270124},
doi = {10.4230/LIPIcs.FSCD.2026},
annote = {Keywords: LIPIcs, Volume 378, FSCD 2026, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{pfenning:LIPIcs.FSCD.2026.0,
author = {Pfenning, Frank},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {0:i--0:xviii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.0},
URN = {urn:nbn:de:0030-drops-270118},
doi = {10.4230/LIPIcs.FSCD.2026.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Sheaves as Oracle Computations (Invited Talk)
Abstract
In type theory, an oracle may be specified abstractly by a predicate whose domain is the type of queries asked of the oracle, and whose proofs are the oracle answers. Such a specification induces an oracle modality that captures a computational intuition about oracles: at each step of reasoning we either know the result, or we ask the oracle a query and proceed upon receiving an answer. We characterize an oracle modality as the least one forcing the given predicate. We establish an adjoint retraction between modalities and propositional containers, from which it follows that every modality is an oracle modality. The left adjoint maps sums to suprema, which makes suprema of modalities easy to compute when they are given in terms of oracle modalities. We also study sheaves for oracle modalities. We describe sheafification in terms of a quotient-inductive type of computation trees, and describe sheaves as algebras for the corresponding monad. We also introduce equifoliate trees, an intensional notion of oracle computation given by a (non-propositional) container. Equifoliate trees descend to sheaves, and modally cover them. As an application, we give a concrete description of all Lawvere-Tierney topologies in a realizability topos, closely related to a game-theoretic characterization by Takayuki Kihara.
Cite as
Danel Ahman and Andrej Bauer. Sheaves as Oracle Computations (Invited Talk). In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 1:1-1:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{ahman_et_al:LIPIcs.FSCD.2026.1,
author = {Ahman, Danel and Bauer, Andrej},
title = {{Sheaves as Oracle Computations}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {1:1--1:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.1},
URN = {urn:nbn:de:0030-drops-263510},
doi = {10.4230/LIPIcs.FSCD.2026.1},
annote = {Keywords: modality, oracle, sheaf}
}
Document
Invited Talk
Saturation-Guided Inductive Synthesis (Invited Talk)
Abstract
Proof by induction is common-place in mathematics [Josef Urban and Geoff Sutcliffe, 2010; Martin Desharnais et al., 2022], formal verification [Raven Beutner and Bernd Finkbeiner, 2024; Wolfgang Ahrendt et al., 2000; Pamina Georgiou et al., 2022], cybersecurity [Simon Jeanteur et al., 2024; Evan Laufer et al., 2024], and many more areas. This talk overviews recent progress in automating inductive reasoning in quantified logic, with applications to code synthesis. Key to our work is saturation-based first-order theorem proving [Laura Kovács and Andrei Voronkov, 2013], using variants of the superposition calculus [Robert Nieuwenhuis and Albert Rubio, 2001]. We show that induction and synthesis are better together in saturation, allowing us not only to prove quantified properties F, but also generate a functional implementation of F during proof search. We showcase our results using the first-order theorem prover Vampire [Filip Bártek et al., 2025], a completely automatic push-button theorem prover for first-order logic with theories, including arithmetic, inductively defined datatypes, induction, and higher-order logic.
We structure our talk within three inter-connected parts.
First, we overview the main ingredients behind saturation provers [Filip Bártek et al., 2025; Stephan Schulz et al., 2019; Christoph Weidenbach et al., 2009] using superposition. Such provers work by negating an input conjecture F, transforming ¬ F into a clausal normal form, and using superposition inferences to derive new clauses from existing ones until a contradiction is reached; when a contradiction is derived, validity of F is established. Many years of development in saturation-based theorem proving have gone into making this process as efficient as possible, while deriving new clauses only when needed in order to tame growth of the search space. Doing so, highly-efficient superposition calculi parametrized by so-called clause selection functions have been proposed, in order to make as few inferences between clauses as possible. Redundancy elimination techniques further prune the search space.
Next, we show how to formalize applications of induction in the saturation process [Márton Hajdú et al., 2022], without bringing drastic changes into the overall framework of first-order proving. A natural choice for implementing induction would be by reducing goals to subgoals, in particular by proving a base case and an inductive step case of a valid induction principle. For example, a goal ∀ x. F(x) over natural numbers x can be proven using structural induction: we prove F[0] (base case) and ∀ x. F(x) ⇒ F(x+1) (step case). However, saturation theorem proving is not about reducing goals to subgoals: in principle, each clause in the search space can be chosen during any step of saturation. We therefore automate induction in saturation as follows. When a clause F(x) is chosen and inductive reasoning over F should be applied (for example, because F uses inductively defined data types x, such as natural numbers), we combine the application of a valid induction schema over F(x) with resolution. Put it simply, induction and resolution are combined in one step of saturation, allowing us to use parts of F(x) as subgoals of F(x). Interestingly with this approach is that clauses generated during saturation may be stronger than the induction schema and, most importantly, are friendly to saturation provers: they are mostly quantifier-free Horn clauses and their (at most one) positive equality cannot be used in many inferences during saturation. Thus, applying many induction inferences during proof search would hardly affect the performance of a saturation prover. Figure 1 lists a property over natural numbers: every natural number x is the half of another natural number y. Proving this property in saturation, and in particular using Vampire, can be achieved by (structural) induction over x.
Finally, we extend saturation proof search with code synthesis [Petra Hozzová et al., 2024]. While proving formula F, we track the constructive parts of the proof of F using so-called answer literals [Cordell Green, 1969]. We use these parts to synthesize a program satisfying F and use the applications of induction in saturation to construct recursive programs satisfying F. In a nutshell, the base case and inductive case steps of induction in saturation express how to construct the desired program for the next recursive step using the program for the previous recursive step; we capture this information via answer literals. When we apply induction in saturation, we introduce a special term into the answer literal and record the program corresponding to the induction step. As we prove induction steps, we capture their corresponding programs in the answer literal. Finally, we convert the special tracker terms from the answer literals into recursive functions, and obtain a program satisfying property F. For example, from the proof of property of Figure 1, our approach implemented in Vampire infers the following functional implementation of a recursive function r, while using only the signature of Figure 1:
𝗋(0) & := 0
𝗋(s(x)) & := s(s(𝗋(x)))
The above inferred function r satisfies the property of Figure 1 and, for each input natural number x, computes a natural number 𝗋(x) such that x is half of 𝗋(x).
In summary, induction and synthesis are better together in saturation-based theorem proving using the superposition calculus. Soundness and practical use of our work has been addressed and experimented using the Vampire theorem prover, both in the case of automating induction [Márton Hajdú et al., 2022; Márton Hajdú et al., 2024] and program synthesis [Petra Hozzová et al., 2023; Petra Hozzová et al., 2024]. Interesting questions regarding completeness arise: if a program satisfying a given property exists, can we derive it from saturation-based proof search? Our recent results [Hajdu et al., 2026] answer this question for recursion-free program using additional assumptions of realizability. A natural direction for future work is to identify realizability assumptions for recursive program synthesis and induction.
Cite as
Laura Kovács. Saturation-Guided Inductive Synthesis (Invited Talk). In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{kovacs:LIPIcs.FSCD.2026.2,
author = {Kov\'{a}cs, Laura},
title = {{Saturation-Guided Inductive Synthesis}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {2:1--2:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.2},
URN = {urn:nbn:de:0030-drops-263521},
doi = {10.4230/LIPIcs.FSCD.2026.2},
annote = {Keywords: automated reasoning, first-order theorem proving, saturation, induction, program synthesis}
}
Document
Proof Identity and Categorical Models of BV
Abstract
BV-categories are a recent development that aims to give categorical semantics to proofs in the logic BV. However, due to the absence of a coherence theorem on one side and a well-defined notion of proof identity for BV on the other side, the precise relation between BV-categories and the logic BV is still not clear. To improve on this situation, we define in this paper a notion of proof identity for BV, based on the notion of atomic flows, which can be seen as a special form of string diagrams. Based on this notion of proof identity, we then strengthen the existing notion of BV-category and prove that it is sound with respect to the logic.
Cite as
Matteo Acclavio, Lutz Straßburger, and Vladimir Zamdzhiev. Proof Identity and Categorical Models of BV. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 3:1-3:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{acclavio_et_al:LIPIcs.FSCD.2026.3,
author = {Acclavio, Matteo and Stra{\ss}burger, Lutz and Zamdzhiev, Vladimir},
title = {{Proof Identity and Categorical Models of BV}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {3:1--3:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.3},
URN = {urn:nbn:de:0030-drops-263532},
doi = {10.4230/LIPIcs.FSCD.2026.3},
annote = {Keywords: BV, Categorical Semantics, Denotational Semantics}
}
Document
Strong Normalisation for Asynchronous Effects
Abstract
Asynchronous effects of Ahman and Pretnar complement the conventional synchronous treatment of algebraic effects with asynchrony based on decoupling the execution of algebraic operation calls into signalling that an operation’s implementation needs to be executed, and into interrupting a running computation with the operation’s result, to which the computation can react by installing matching interrupt handlers. Beyond providing asynchrony for algebraic effects, the resulting core calculus also naturally models examples such as pre-emptive multi-threading, (cancellable) remote function calls, and multi-party applications. In this paper, we study the normalisation properties of this calculus. We prove that if one removes general recursion from it, then the remaining calculus is strongly normalising, including both its sequential and parallel parts. To cover more interesting programs, we also prove that the sequential part of the calculus remains strongly normalising when a controlled amount of interrupt-driven recursive behaviour is reintroduced. Our normalisation proofs are structured compositionally as an extension of Lindley and Stark’s ⊤⊤-lifting-based approach for proving strong normalisation of effectful languages. All our results are also formalised in Agda.
Cite as
Danel Ahman and Ilja Sobolev. Strong Normalisation for Asynchronous Effects. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{ahman_et_al:LIPIcs.FSCD.2026.4,
author = {Ahman, Danel and Sobolev, Ilja},
title = {{Strong Normalisation for Asynchronous Effects}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {4:1--4:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.4},
URN = {urn:nbn:de:0030-drops-263541},
doi = {10.4230/LIPIcs.FSCD.2026.4},
annote = {Keywords: Strong normalisation, Girard-Tait method, reducibility, asynchronous effects}
}
Document
Not Choosing Is Still a Choice: Constructive mathematics without any choice
Abstract
The axiom of choice (AC) states that every total relation contains a function. It enjoys a pivotal role in both classical and constructive dialects of mathematics. In the former, it is seen as a useful closure property invoked especially in set-theoretic contexts, in the latter it is seen either as a tautology, following from a constructive reading of totality proofs, or as a taboo, as by an extensional reading of totality proofs it enforces full classical logic. It has therefore been debated how much of AC should be accepted in constructive foundations and authors like Richman argued for
"Constructive mathematics without choice"
where even countable choice, not immediately jeopardising constructive reasoning, is avoided.
With this paper, we propose a continuation of Richman’s programme of more radical extent and systematically study constructive foundations absent of countable, unique, or quantifier-free choice principles as well as the spurious fragments of (the actual) AC in form of extensionality principles:
"Constructive mathematics without any choice"
We argue that such a minimalistic setting is advantageous, for instance for studies in constructive reverse mathematics and synthetic computability theory. Apart from these programmatic considerations and a careful encyclopedia of choice principles, we revisit and refine several results from the literature: We show that already the partition principle (a consequence of AC of unknown strength) implies the excluded middle, that already logically decidable (inductive) equality of propositions implies proof irrelevance, and that function inversion principles such as the Cantor-Bernstein theorem not only rely on the excluded middle but also on unique choice. To the best of our knowledge, the latter is the first reverse mathematics result regarding the full axiom of unique choice, enabled by our minimal setting. Implementing such a minimalistic foundation, the proofs of all our results have been mechanised with the Rocq prover.
Cite as
Martin Baillon, Yannick Forster, Dominik Kirst, Assia Mahboubi, and Pierre-Marie Pédrot. Not Choosing Is Still a Choice: Constructive mathematics without any choice. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 5:1-5:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{baillon_et_al:LIPIcs.FSCD.2026.5,
author = {Baillon, Martin and Forster, Yannick and Kirst, Dominik and Mahboubi, Assia and P\'{e}drot, Pierre-Marie},
title = {{Not Choosing Is Still a Choice: Constructive mathematics without any choice}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {5:1--5:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.5},
URN = {urn:nbn:de:0030-drops-263553},
doi = {10.4230/LIPIcs.FSCD.2026.5},
annote = {Keywords: Axiom of Choice, Constructive Mathematics, Type Theory}
}
Document
Simpler Presentations for Many Fragments of Quantum Circuits
Abstract
Equational reasoning is central to quantum circuit optimisation and verification: one replaces subcircuits by provably equivalent ones using a fixed set of rewrite rules viewed as equations. A finite rule set is most informative when it separates the genuine algebra of a circuit fragment from the structural treatment of wires. This paper gives six near-Clifford fragments a common PROP treatment, where wire permutations are structural: qubit Clifford, real Clifford, Clifford+T (up to two qubits), Clifford+CS (up to three qubits), CNOT-dihedral, and qutrit Clifford. Starting from prior completeness theorems, we transfer completeness into this setting and remove redundant non-structural rules, then check minimality by separating interpretations tailored to individual axioms; the resulting presentations are minimal in all arities for qubit Clifford, real Clifford, and CNOT-dihedral, minimal in bounded ranges for the remaining fragments, and comparable by one transfer-and-separation pattern.
Cite as
Colin Blake. Simpler Presentations for Many Fragments of Quantum Circuits. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{blake:LIPIcs.FSCD.2026.6,
author = {Blake, Colin},
title = {{Simpler Presentations for Many Fragments of Quantum Circuits}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {6:1--6:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.6},
URN = {urn:nbn:de:0030-drops-263562},
doi = {10.4230/LIPIcs.FSCD.2026.6},
annote = {Keywords: Quantum circuits, Clifford group, equational theories, minimality, qutrit}
}
Document
Graphical Symplectic Algebra
Abstract
We introduce a family of diagrammatical equational theories unifying two research programs: categorical quantum mechanics and graphical linear algebra. We prove their completeness with respect to denotational semantics described in terms of relations between vector spaces equipped with symplectic structure. This provides versatile graphical languages encompassing both affinely constrained classical mechanical systems, as well as odd-prime-dimensional stabiliser and Gaussian quantum circuits. Terms are described by labelled graphs with input and output interfaces, and the languages are equipped with equational theories amenable to standard graph rewriting techniques.
In order to reason about large composite systems, we introduce a compact scalable notation where the vertices are themselves labelled by graphs. This notation allows us to state new and powerful rewrite rules which operate on diagrams at a large scale. We also show how this notation neatly captures some important constructions, such as graph states of quantum computing and the impedance and admittance matrices of electrical networks.
Cite as
Robert I. Booth, Titouan Carette, and Cole Comfort. Graphical Symplectic Algebra. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 7:1-7:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{booth_et_al:LIPIcs.FSCD.2026.7,
author = {Booth, Robert I. and Carette, Titouan and Comfort, Cole},
title = {{Graphical Symplectic Algebra}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {7:1--7:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.7},
URN = {urn:nbn:de:0030-drops-263573},
doi = {10.4230/LIPIcs.FSCD.2026.7},
annote = {Keywords: graphical algebra, symplectic geometry, string diagrams, category theory, classical mechanics, quantum mechanics, graph theory}
}
Document
Denotational Semantics for Stabiliser Quantum Programs
Abstract
The stabiliser fragment of quantum theory is a foundational building block for quantum error correction, and hence for the fault-tolerant compilation of quantum programs. In this article, we develop a sound, universal, and complete denotational semantics for stabiliser operations, including measurement, classically controlled Pauli operators, and affine classical computation, thereby supporting an explicit treatment of quantum error-correcting codes. We interpret stabiliser operations as affine relations over finite fields, yielding a semantics that reflects the algebraic structure underlying stabiliser quantum error correction. Because stabiliser quantum mechanics has a well-behaved algebraic structure, our relational semantics is conceptually transparent and computationally tractable when compared to standard denotational models for general quantum programs. We demonstrate the resulting semantics by describing a small, low-level assembly language for stabiliser programs with fully abstract denotational semantics.
Cite as
Robert I. Booth and Cole Comfort. Denotational Semantics for Stabiliser Quantum Programs. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 8:1-8:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{booth_et_al:LIPIcs.FSCD.2026.8,
author = {Booth, Robert I. and Comfort, Cole},
title = {{Denotational Semantics for Stabiliser Quantum Programs}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {8:1--8:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.8},
URN = {urn:nbn:de:0030-drops-263580},
doi = {10.4230/LIPIcs.FSCD.2026.8},
annote = {Keywords: quantum programming languages, quantum error correction, denotational semantics, categorical semantics, stabiliser theory, symplectic linear algebra}
}
Document
Groups and Inverse Semigroups in Lambda Calculus
Abstract
We study invertibility of λ-terms modulo λ-theories. Here a fundamental role is played by a class of λ-terms called finite hereditary permutations (FHP) and by their infinite generalisations (HP). More precisely, FHPs are the invertible elements in the least extensional λ-theory λ η and HPs are those in the greatest sensible λ-theory H^*. Our approach is based on inverse semigroups, algebraic structures that generalise groups and semilattices. We show that FHP modulo a λ-theory T is always an inverse semigroup and that HP modulo T is an inverse semigroup whenever T contains the theory of Böhm trees. An inverse semigroup comes equipped with a natural order. We prove that the natural order corresponds to η-expansion in FHP/T, and to infinite η-expansion in HP/T. Building on these correspondences we obtain the two main contributions of this work: firstly, we recast in a broader framework the results cited at the beginning; secondly, we prove that the FHPs are the invertible λ-terms in all the λ-theories lying between λ η and H^+. The latter is Morris' observational λ-theory, defined by using the β-normal forms as observables.
Cite as
Antonio Bucciarelli, Arturo De Faveri, Giulio Manzonetto, and Antonino Salibra. Groups and Inverse Semigroups in Lambda Calculus. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 9:1-9:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bucciarelli_et_al:LIPIcs.FSCD.2026.9,
author = {Bucciarelli, Antonio and De Faveri, Arturo and Manzonetto, Giulio and Salibra, Antonino},
title = {{Groups and Inverse Semigroups in Lambda Calculus}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {9:1--9:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.9},
URN = {urn:nbn:de:0030-drops-263596},
doi = {10.4230/LIPIcs.FSCD.2026.9},
annote = {Keywords: Lambda Calculus, Invertibility, Groups, Inverse Semigroups}
}
Document
Equational Reasoning in Languages with Binders via Permutation Fixed-Points
Abstract
Equational reasoning with binders and structural congruence is difficult due to the interaction between name binding and algebraic laws. Equational theories such as commutativity induce forms of permutation invariance on names that are not captured by standard approaches to the formalisation of syntax with binders.
We show that in the nominal setting, this limitation can be addressed by using generalised permutation fixed-point constraints to make invariance explicit. This yields a uniform framework for reasoning about equality of nominal terms modulo α-equivalence and arbitrary equational theories. We introduce a proof system and show that it is sound and complete with respect to a nominal-set semantics, which explains how symmetry can be internalised via fixed-point constraints viewed as N-quantified stabiliser conditions. We provide examples in Milner’s π-calculus - a well-known model of concurrent computation that includes binders and non-trivial structural congruences.
Cite as
Ali K. Caires-Santos, Maribel Fernández, Murdoch James Gabbay, and Daniele Nantes-Sobrinho. Equational Reasoning in Languages with Binders via Permutation Fixed-Points. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 10:1-10:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{cairessantos_et_al:LIPIcs.FSCD.2026.10,
author = {Caires-Santos, Ali K. and Fern\'{a}ndez, Maribel and Gabbay, Murdoch James and Nantes-Sobrinho, Daniele},
title = {{Equational Reasoning in Languages with Binders via Permutation Fixed-Points}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {10:1--10:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.10},
URN = {urn:nbn:de:0030-drops-263609},
doi = {10.4230/LIPIcs.FSCD.2026.10},
annote = {Keywords: Binding, alpha-equivalence, nominal algebra, permutation fixed-point}
}
Document
Approximation Theory for Distant Bang Calculus
Abstract
Approximation semantics capture the observable behaviour of λ-terms. Böhm Trees and Taylor Expansion are its two central paradigms, related by the Commutation Theorem. While these notions are well understood in Call-by-Name (CbN), they have only recently been developed for Call-by-Value (CbV), which motivate the search for a unified approximation framework. The Bang-calculus provides such a framework: it subsumes both CbN and CbV through linear-logic translations and enjoys robust rewriting properties. We develop the approximation semantics of dBang (the Bang-calculus with explicit substitutions and distant reductions) by introducing approximation trees in the Böhm tradition together with Taylor expansion. We establish their fundamental properties, including a commutation theorem. Via translations, our results recover the CbN and CbV cases within a single unifying framework capturing infinitary and resource-sensitive semantics.
Cite as
Kostia Chardonnet, Jules Chouquet, and Axel Kerinec. Approximation Theory for Distant Bang Calculus. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{chardonnet_et_al:LIPIcs.FSCD.2026.11,
author = {Chardonnet, Kostia and Chouquet, Jules and Kerinec, Axel},
title = {{Approximation Theory for Distant Bang Calculus}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {11:1--11:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.11},
URN = {urn:nbn:de:0030-drops-263612},
doi = {10.4230/LIPIcs.FSCD.2026.11},
annote = {Keywords: Lambda-calculus, B\"{o}hm Trees, Taylor expansion of lambda-terms}
}
Document
Resource-Aware Quantum Programming with General Recursion and Quantum Control
Abstract
This paper introduces the hybrid quantum language with general recursion {{Hyrql}}, driven towards resource-analysis. By design, {{Hyrql}} does not require the specification of an initial set of quantum gates. Hence, it is well amenable towards a generic cost analysis, unlike languages that use different sets of quantum gates, which yield quantum circuits of distinct complexity.
Regarding resource-analysis, we show how to relate the runtime of an expressive fragment of {{Hyrql}} programs with the size of the corresponding quantum circuits. We also manage to capture the class of functions computable in quantum polynomial time, which, by Yao’s Theorem, corresponds to families of circuits of polynomial size. Consequently, this result paves the way for the use of termination and runtime-analysis techniques designed for classical programs to guarantee bounds on the size of quantum circuits.
Cite as
Kostia Chardonnet, Emmanuel Hainry, Romain Péchoux, and Thomas Vinet. Resource-Aware Quantum Programming with General Recursion and Quantum Control. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{chardonnet_et_al:LIPIcs.FSCD.2026.12,
author = {Chardonnet, Kostia and Hainry, Emmanuel and P\'{e}choux, Romain and Vinet, Thomas},
title = {{Resource-Aware Quantum Programming with General Recursion and Quantum Control}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {12:1--12:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.12},
URN = {urn:nbn:de:0030-drops-263626},
doi = {10.4230/LIPIcs.FSCD.2026.12},
annote = {Keywords: Hybrid Quantum Programs, Resource Analysis}
}
Document
Evidence-Tracked Tape Semantics for Probabilistic Computation
Abstract
A standard intensional account of probabilistic computation represents a randomized program as a deterministic computation that consumes an explicit random tape. This yields a two-layer perspective: an intensional layer that makes reuse of randomness and correlation visible, and an extensional layer obtained by interpreting tapes under a chosen probability measure. We develop an evidence-tracked tape semantics using the monadic-core-to-evidenced-frame pipeline (and its induced realizability tripos), obtaining a higher-order logic in which entailments are witnessed by uniform evidence transformers. Quantitative statements are recovered by interpretation: once a tape measure is fixed, probabilities and expectations arise by extracting numerical summaries from tape-indexed predicates, and entailments yield sound inequalities, with an almost-sure quotient supporting probability-one reasoning. We also study intensional principles that are lost at the level of laws, including proof-relevant transport along realizable tape-rewiring maps and a canonical splitting discipline for stream tapes enforcing independent draws. Finally, we relate tape-based reasoning to an extensional law semantics via pushforward, isolating a probability-one must abstraction as a sound summary of tape-based proofs.
Cite as
Liron Cohen and Tomer Samara. Evidence-Tracked Tape Semantics for Probabilistic Computation. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{cohen_et_al:LIPIcs.FSCD.2026.13,
author = {Cohen, Liron and Samara, Tomer},
title = {{Evidence-Tracked Tape Semantics for Probabilistic Computation}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {13:1--13:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.13},
URN = {urn:nbn:de:0030-drops-263633},
doi = {10.4230/LIPIcs.FSCD.2026.13},
annote = {Keywords: probabilistic programming, random tapes, realizability, evidenced frames, program logic, monadic combinatory algebras}
}
Document
How Term Rewriting Structures Shape the Decidability of Knowledge Problems
Abstract
Deduction and static equivalence are central knowledge problems in the formal analysis of security protocols and are known to be undecidable for general equational theories. Several decidable classes have been identified through structural restrictions, including subterm convergent theories, shallow permutative theories, contracting theories and some are implemented in tools such as ProVerif and DeepSec.
We identify two recurring themes: symbol preservation, where symbols are maintained across axioms, and symbol contraction, where symbols decrease in depth or number from left to right.
For symbol-preserving systems, we introduce measure-invariant (MI) and separate measure-invariant (SMI) theories, generalizing permutative classes and providing new decidable fragments for deduction and static equivalence. Depth-sensitive refinements, including depth-preserving permutative (DPP) and depth-preserving variable-permuting (DPVP) theories, are case studies to understand whether the depth of occurrences of symbols matter. For symbol-contraction systems, we define depth-decreasing (DD) and variable-preserving function-decreasing (VBFD) theories, capturing some simple relaxations of term contraction; while deduction is undecidable in general, these restrictions highlight potential decidable fragments.
Overall, our results show that controlling symbol dynamics in rewrite rules provides a unifying perspective on the decidability of knowledge problems, offering conceptual clarity on what makes these problems hard for different equational theories.
Cite as
Raja O. P. Damanik and Alwen Tiu. How Term Rewriting Structures Shape the Decidability of Knowledge Problems. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{damanik_et_al:LIPIcs.FSCD.2026.14,
author = {Damanik, Raja O. P. and Tiu, Alwen},
title = {{How Term Rewriting Structures Shape the Decidability of Knowledge Problems}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {14:1--14:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.14},
URN = {urn:nbn:de:0030-drops-263649},
doi = {10.4230/LIPIcs.FSCD.2026.14},
annote = {Keywords: Security Protocol, Intruder Deduction, Static Equivalence, Term Rewriting}
}
Document
Undecidability for Semirings with Fixed Points
Abstract
In this work, we prove the undecidability (and Σ⁰₁-completeness) of several theories of semirings with fixed points. The generality of our results stems from recursion theoretic methods, namely the technique of effective inseparability. Our result applies to many theories proposed in the literature, including Conway μ-semirings, Park μ-semirings, and Chomsky algebras.
Cite as
Anupam Das, Abhishek De, and Stepan L. Kuznetsov. Undecidability for Semirings with Fixed Points. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{das_et_al:LIPIcs.FSCD.2026.15,
author = {Das, Anupam and De, Abhishek and Kuznetsov, Stepan L.},
title = {{Undecidability for Semirings with Fixed Points}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {15:1--15:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.15},
URN = {urn:nbn:de:0030-drops-263650},
doi = {10.4230/LIPIcs.FSCD.2026.15},
annote = {Keywords: Semirings, fixed points, decidability, context-free, inseparability}
}
Document
Quantum Bayesian Networks: Compositionality and Typing via Linear Logic
Abstract
Quantum Bayesian networks [Henson et al., 2014] provide a mathematical formalism to describe causal relations, to analyse correlations, and to predict the probabilities of measurement outcomes, in systems involving both classical and quantum data. They generalize Pearl’s Bayesian networks [Pearl, 2009] - prominent graphical models for classical probabilistic reasoning and inference.
The goal of this paper is to bring compositional principles and a typing discipline into this setting. A key feature of our compositional semantics is that when all causes are classical, it coincides with the standard factor-based semantics of Bayesian networks, while in the purely quantum case it reduces to tensor networks. We then propose a typed formalism based on linear logic proof-nets, where types ensure well-behaved composition of systems, and which we prove sound and complete with respect to quantum Bayesian networks.
Cite as
Rémi Di Guardia, Thomas Ehrhard, and Claudia Faggian. Quantum Bayesian Networks: Compositionality and Typing via Linear Logic. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 16:1-16:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{diguardia_et_al:LIPIcs.FSCD.2026.16,
author = {Di Guardia, R\'{e}mi and Ehrhard, Thomas and Faggian, Claudia},
title = {{Quantum Bayesian Networks: Compositionality and Typing via Linear Logic}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {16:1--16:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.16},
URN = {urn:nbn:de:0030-drops-263668},
doi = {10.4230/LIPIcs.FSCD.2026.16},
annote = {Keywords: Quantum Bayesian Networks, Quantum Causal Models, Bayesian Networks, Proof-Nets, Linear Logic}
}
Document
A Bounded Parallel Intersection Type System
Abstract
We introduce a new presentation of the intersection type discipline in which typing judgments derive vectors of types rather than single types. The system uses binary relations to control the flow of information between coordinates of these vectors. We refer to this presentation as system R. The maximal length of type vectors assigned to variables serves as a reasonable notion of dimension for system R, which allows for a natural stratification into fragments of bounded dimension.
The present system lies strictly between two known bounded-dimensional systems: the multiset-dimensional system, for which inhabitation is EXPSPACE-complete, and the set-dimensional system, for which inhabitation is undecidable. Our main result is that inhabitation in bounded system R is decidable in 2-EXPTIME, while for each fixed dimension, inhabitation is decidable in EXPTIME. This result is based on a subformula property restricting the inhabitant search space. Unlike in traditional intersection type systems, the proof of the subformula property requires careful treatment of the additional information flow management capabilities.
Finally, we argue that system R and its stratification is a valid presentation of the intersection type discipline. First, by proving the subject reduction property for system R in each bounded dimension, and second, by establishing a correspondence with the classical intersection type system of Barendregt, Coppo, and Dezani-Ciancaglini.
Cite as
Andrej Dudenhefner, Aleksy Schubert, and Jakob Rehof. A Bounded Parallel Intersection Type System. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{dudenhefner_et_al:LIPIcs.FSCD.2026.17,
author = {Dudenhefner, Andrej and Schubert, Aleksy and Rehof, Jakob},
title = {{A Bounded Parallel Intersection Type System}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {17:1--17:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.17},
URN = {urn:nbn:de:0030-drops-263679},
doi = {10.4230/LIPIcs.FSCD.2026.17},
annote = {Keywords: type system, lambda-calculus, intersection types, inhabitation, complexity}
}
Document
Ground Stratified Inductive Definitions
Abstract
Logics of definitions extend first order intuitionistic logic with fixed-point definitions which associate formulas to atomic predicates. These associated formulas must be constrained for consistency. In the original formulation, predicate symbols were required to be ordered and only predicates lower in the order were allowed to appear negatively in the defining formula. This constraint renders ineligible definitions such as those of logical relations in which the predicate being defined must be allowed to appear negatively, albeit with smaller arguments. Tiu has formalized a weaker constraint called ground stratification that permits such definitions and has shown that it suffices for consistency. Definitions can also be given a least fixed-point interpretation via a special induction rule. We address the question of whether Tiu’s relaxation carries over to such a treatment. We propose a new induction rule for ground stratified inductive definitions that takes into account the fact that the definition of the predicate in question must itself be considered to be stratified by the complexity of its arguments to obtain a least fixed-point interpretation. We establish the consistency of the resulting logic and we illustrate its new capabilities via an example that encodes a strong normalizability proof for the simply typed λ-calculus in which the reducibility predicate is inductively defined by recursion on its arguments.
Cite as
Nathan Guermond and Gopalan Nadathur. Ground Stratified Inductive Definitions. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 18:1-18:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{guermond_et_al:LIPIcs.FSCD.2026.18,
author = {Guermond, Nathan and Nadathur, Gopalan},
title = {{Ground Stratified Inductive Definitions}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {18:1--18:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.18},
URN = {urn:nbn:de:0030-drops-263685},
doi = {10.4230/LIPIcs.FSCD.2026.18},
annote = {Keywords: Logic of definitions, induction, cut-elimination, consistency}
}
Document
Abstract Framework for All-Path Reachability Analysis toward Safety and Liveness Verification
Abstract
An all-path reachability (APR, for short) predicate over an object set is a pair of a source set and a target set, which are subsets of the object set. APR predicates have been defined for abstract reduction systems (ARSs, for short) and then extended to logically constrained term rewrite systems (LCTRSs, for short) as pairs of constrained terms that represent sets of terms modeling configurations, states, etc. An APR predicate is partially (or demonically) valid w.r.t. a rewrite system if every finite maximal reduction sequence of the system starting from any element in the source set includes an element in the target set. Partial validity of APR predicates w.r.t. ARSs is defined by means of two inference rules, which can be considered a proof system to construct (possibly infinite) derivation trees for partial validity. On the other hand, a proof system for LCTRSs consists of four inference rules, leaving a gap between the inference rules for ARSs and LCTRSs. In this paper, we revisit the framework for APR analysis and adapt it to verification of not only safety but also liveness properties. To this end, we first reformulate an abstract framework for partial validity w.r.t. ARSs so that there is a one-to-one correspondence between the inference rules for partial validity w.r.t. ARSs and LCTRSs. Secondly, we show how to apply APR analysis to safety verification. Thirdly, to apply APR analysis to liveness verification, we introduce a novel stronger validity of APR predicates, called total validity, which requires not only finite but also infinite execution paths to reach target sets. Finally, for a partially valid APR predicate with a cyclic-proof tree, we show that the acyclicity of the proof graph obtained from the cyclic-proof tree is a necessary and sufficient condition for total validity. The condition implies that if there exists a cyclic-proof tree for an APR predicate, the proof graph of which is acyclic, then the APR predicate is totally valid.
Cite as
Misaki Kojima and Naoki Nishida. Abstract Framework for All-Path Reachability Analysis toward Safety and Liveness Verification. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{kojima_et_al:LIPIcs.FSCD.2026.19,
author = {Kojima, Misaki and Nishida, Naoki},
title = {{Abstract Framework for All-Path Reachability Analysis toward Safety and Liveness Verification}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {19:1--19:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.19},
URN = {urn:nbn:de:0030-drops-263690},
doi = {10.4230/LIPIcs.FSCD.2026.19},
annote = {Keywords: abstract reduction system, reachability, cyclic proof, runtime-error verification}
}
Document
Relational Dualities and Bisimulation
Abstract
The Kripke semantics of various logics arises via categorical dualities between a category of relational frames and their maps, and a category of algebras and logical homomorphisms. When the relational frames are considered as computational systems (e.g. the states of a machine), the corresponding algebra is one of logical predicates on these systems (e.g. predicates on these states, i.e. program logics). Our aim is to extend this phenomenon to relations, putting well-behaved relations between systems (e.g. bisimulations) in correspondence with relations between predicates. This is achieved by constructing particular relational extensions of Tarski duality (for infinitary classical propositional logic) and Thomason duality (for infinitary classical modal logic). We sketch how these dualities give rise to a proof system that relates formulae between different systems.
Cite as
Piotr Kozicki and G. A. Kavvos. Relational Dualities and Bisimulation. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{kozicki_et_al:LIPIcs.FSCD.2026.20,
author = {Kozicki, Piotr and Kavvos, G. A.},
title = {{Relational Dualities and Bisimulation}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {20:1--20:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.20},
URN = {urn:nbn:de:0030-drops-263703},
doi = {10.4230/LIPIcs.FSCD.2026.20},
annote = {Keywords: bisimulation, modal logic, duality, categorical semantics}
}
Document
Constructing (Co)inductive Types via Large Sizes
Abstract
To ensure decidability and consistency of its type theory, a proof assistant should only accept terminating recursive functions and productive corecursive functions. Most proof assistants enforce this through syntactic conditions, which can be restrictive and non-modular. Sized types are a type-based alternative where (co)inductive types are annotated with additional size information. Well-founded induction on sizes can then be used to prove termination and productivity.
An implementation of sized types exists in Agda, but it is currently inconsistent due to the addition of a largest size. We investigate an alternative approach, where intensional type theory is extended with a large type of sizes and parametric quantifiers over sizes. We show that inductive and coinductive types can be constructed in this theory, which improves on earlier work where this was only possible for the finitely-branching inductive types. The consistency of the theory is justified by an impredicative realisability model, which interprets the type of sizes as an uncountable ordinal.
Cite as
Bastiaan Laarakker, Daniël Otten, and Benno van den Berg. Constructing (Co)inductive Types via Large Sizes. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{laarakker_et_al:LIPIcs.FSCD.2026.21,
author = {Laarakker, Bastiaan and Otten, Dani\"{e}l and van den Berg, Benno},
title = {{Constructing (Co)inductive Types via Large Sizes}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {21:1--21:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.21},
URN = {urn:nbn:de:0030-drops-263714},
doi = {10.4230/LIPIcs.FSCD.2026.21},
annote = {Keywords: Sized Types, Parametricity, Realisability, Impredicativity, Constructive Ordinals, (Co)inductive Types}
}
Document
Non-Wellfounded Derivations for Intersection Subtyping with Fixpoints
Abstract
Subtyping is a key ingredient of many intersection type systems. In the case of the BCD system, B. Pierce gave a transitivity-free presentation of subtyping. This provides better structural properties for the analysis of this relation and leads to a simple decision algorithm.
We generalize this transitivity-free approach to a general class of extensions of BCD allowing to impose some pre-order as well as some fixpoint equations on atoms. This includes in particular the case of various intersection type systems compatible with η-equality (Scott, Park, etc.).
Proving the equivalence between the transitivity-free systems and their BCD-style presentation is addressed by means of cut-elimination techniques from proof theory. Due to the presence of fixpoints, we are led to introduce non-wellfounded derivations. In the context of the structural analysis of intersection subtyping, this happens to be the first use of infinitary derivations.
Cite as
Olivier Laurent and Jui-Hsuan Wu. Non-Wellfounded Derivations for Intersection Subtyping with Fixpoints. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{laurent_et_al:LIPIcs.FSCD.2026.22,
author = {Laurent, Olivier and Wu, Jui-Hsuan},
title = {{Non-Wellfounded Derivations for Intersection Subtyping with Fixpoints}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {22:1--22:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.22},
URN = {urn:nbn:de:0030-drops-263721},
doi = {10.4230/LIPIcs.FSCD.2026.22},
annote = {Keywords: Intersection types, subtyping, non-wellfounded proofs, fixpoints, cut elimination}
}
Document
Universal Properties of Petri Net Unfoldings
Abstract
It is an established idea in concurrency theory that every Petri net admits an unfolding semantics. This is a denotational object that represents its domain of possible executions. Unfoldings play an important role in practical analysis and verification.
This paper is concerned with the following well-known problem: while the unfolding resembles a universal construction in the category of Petri nets, it generally fails to satisfy the expected universal property. This is because the unfolding construction overlooks the net’s internal symmetries.
There are two solutions: make these symmetries explicit to obtain a weak universal property (one that holds only "up to symmetry"); or break the symmetries by assigning individual identities to components of the net. We review these two solutions and establish, in each case, a universal unfolding of Petri nets to event structures.
This paper demonstrates a 2-categorical approach to Petri net unfoldings. We show that each unfolding semantics determines a 2-categorical relative adjunction involving Petri nets and event structures. Viewed in this way, the above two constructions can be related formally via an appropriate morphism of adjunctions. We exhibit a 2-density property of event structures which implies that unfolding functors are essentially unique.
Cite as
Serge Lechenne and Hugo Paquet. Universal Properties of Petri Net Unfoldings. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{lechenne_et_al:LIPIcs.FSCD.2026.23,
author = {Lechenne, Serge and Paquet, Hugo},
title = {{Universal Properties of Petri Net Unfoldings}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {23:1--23:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.23},
URN = {urn:nbn:de:0030-drops-263734},
doi = {10.4230/LIPIcs.FSCD.2026.23},
annote = {Keywords: Petri nets, Event structures, Symmetry, Unfolding, 2-Categories}
}
Document
Treating Congruences as Equalities Within Proofs
Abstract
Gentzen’s sequent calculus is a foundational tool for describing and investigating provability, yet its fine-grained inference rules generally do not directly support automated proof search. Incorporating synthetic inferences improves automatability, but they do not provide mechanisms for reasoning naturally about the elementary mathematical notions of equivalence and congruence. In this paper, we present a first-order framework for reasoning modulo such relations within the sequent calculus. We provide a setting in which congruences can be treated as actual equalities, mirroring the informal practice of mathematicians and eliminating the need to use the lemmas typically required for formal congruence proofs. We demonstrate that this approach remains strictly first-order, avoids the complexity of higher-order or set-theoretic constructions, and yields proof systems that retain essential meta-theoretic properties.
Cite as
Dale Miller. Treating Congruences as Equalities Within Proofs. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{miller:LIPIcs.FSCD.2026.24,
author = {Miller, Dale},
title = {{Treating Congruences as Equalities Within Proofs}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {24:1--24:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.24},
URN = {urn:nbn:de:0030-drops-263748},
doi = {10.4230/LIPIcs.FSCD.2026.24},
annote = {Keywords: Proof theory, equality, equivalences, congruences}
}
Document
The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete
Abstract
In this paper, we show that the equational theory of relational Kleene algebra with the graph loop operator (a.k.a. fixset) is PSpace-complete. Here, the graph loop is the unary operator that restricts a binary relation to the identity relation. We further show that this PSpace-completeness still holds by extending the terms with top, tests, converse, and nominals, over relational models. Notably, for Kleene algebra with tests (KAT), while the equational theory of relational KAT with antidomain is ExpTime-complete, we show that the equational theory of relational KAT with domain is PSpace-complete, thereby resolving a problem left open in previous works.
To this end, we introduce a novel automaton model on relational structures (graphs), called loop-automata. Loop-automata extend nondeterministic finite automata with a transition type that tests whether the current vertex has a loop. Using this model, we can give a polynomial-time reduction from the equational theories above to the language inclusion problem for 2-way alternating automata.
Cite as
Yoshiki Nakamura. The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{nakamura:LIPIcs.FSCD.2026.25,
author = {Nakamura, Yoshiki},
title = {{The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {25:1--25:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.25},
URN = {urn:nbn:de:0030-drops-263758},
doi = {10.4230/LIPIcs.FSCD.2026.25},
annote = {Keywords: Kleene algebra, Graph loop, Domain}
}
Document
Divide and Check: Logical Relations, No Algorithms Attached
Abstract
The correctness of type-checking implementations for proof assistants based on dependent type theory relies on metatheoretical properties that ensure the decidability of typing, some of which require substantial logical strength. Recent mechanizations of such algorithms have highlighted the importance of separating the algorithmic components of the proof - often intricate but requiring relatively low logical strength - from the logical components, which depend on stronger metatheoretical properties, such as normalization or the injectivity of type constructors. In this work, we revisit the logical relations technique and show how it can be used to derive these metatheoretical properties in a direct and uniform way for a core dependent type theory featuring Π-types, N, ⊥ and a universe U. Our presentation yields a compact and conceptually simplified argument that isolates the logically strong reasoning from the algorithmic core. We argue that this approach scales smoothly to richer type theories, and demonstrate this by extending our construction to Exceptional Type Theory (ExcTT), obtaining the first mechanized canonicity proof for this theory.
Cite as
Josselin Poiret, Kenji Maillard, and Nicolas Tabareau. Divide and Check: Logical Relations, No Algorithms Attached. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 26:1-26:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{poiret_et_al:LIPIcs.FSCD.2026.26,
author = {Poiret, Josselin and Maillard, Kenji and Tabareau, Nicolas},
title = {{Divide and Check: Logical Relations, No Algorithms Attached}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {26:1--26:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.26},
URN = {urn:nbn:de:0030-drops-263764},
doi = {10.4230/LIPIcs.FSCD.2026.26},
annote = {Keywords: Type Theory, Proof Assistants}
}
Document
Polymorphism Meets DHOL
Abstract
DHOL is an extensional, classical logic that equips the well-known higher-order logic (HOL) with dependent types. This allows for concise encodings of important domains like size-bounded data structures, category theory, or proof theory. Automation support is obtained by translating DHOL to HOL, for which powerful modern automated theorem provers are available. However, a critically missing feature of DHOL is polymorphism. We develop the syntax and semantics of polymorphic DHOL and extend the translation accordingly. We implement the translation in the logic-embedding tool and evaluate it on a range of TPTP formalizations. The logic-embedding tool, together with an off-the-shelf HOL theorem prover easily creates a PDHOL theorem prover for experimenting.
Cite as
Rhea Ranalter, Florian Rabe, and Cezary Kaliszyk. Polymorphism Meets DHOL. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 27:1-27:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{ranalter_et_al:LIPIcs.FSCD.2026.27,
author = {Ranalter, Rhea and Rabe, Florian and Kaliszyk, Cezary},
title = {{Polymorphism Meets DHOL}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {27:1--27:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.27},
URN = {urn:nbn:de:0030-drops-263774},
doi = {10.4230/LIPIcs.FSCD.2026.27},
annote = {Keywords: Polymorphism, Dependent Types, Higher-order Logic, Automated Reasoning}
}
Document
A Complete Finitary Refinement Type System for Scott-Open Properties
Abstract
We are interested in proving input-output properties of functions that handle infinite data such as streams or non-wellfounded trees. We provide a finitary refinement type system which is (sound and) complete for Scott-open properties defined in a fixpoint-like logic. Working on top of Abramsky’s Domain Theory in Logical Form, we build from the well-known fact that the Scott domains interpreting recursive types are spectral spaces. The usual symmetry between Scott-open and compact-saturated sets is reflected in logical polarities: positive formulae allow for least fixpoints and define Scott-open sets, while negative formulae allow for greatest fixpoints and define compact-saturated sets. A realizability implication with the expected (contra)variance on polarities allows for non-trivial input-output properties to be formulated as positive formulae on function types.
Cite as
Colin Riba and Adam Donadille. A Complete Finitary Refinement Type System for Scott-Open Properties. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{riba_et_al:LIPIcs.FSCD.2026.28,
author = {Riba, Colin and Donadille, Adam},
title = {{A Complete Finitary Refinement Type System for Scott-Open Properties}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {28:1--28:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.28},
URN = {urn:nbn:de:0030-drops-263780},
doi = {10.4230/LIPIcs.FSCD.2026.28},
annote = {Keywords: Domain Theory, Temporal Logic, Refinement Types}
}
Document
Absolute Convergence and Taylor Expansion in Web Based Models of Linear Logic
Abstract
We provide in this paper a generic construction of web models of linear logic with partial sums. Our construction captures a wide class of orthogonality models, ranging from coherence spaces to probabilistic coherence spaces, finiteness spaces and Köthe spaces. All these models are built on the same principles, but were very heterogeneous in the specificities of their technical development. Our construction factorizes these specificities, allowing a unified treatment of further developments, such as differentiation and Taylor expansion.
The differential λ-calculus relates quantitative aspects of programs to differentiation and to Taylor expansion in models of linear logic. Recent work has generalized the axioms of Taylor expansion, so that they apply to many models that only feature partial sums. However, that work did not cover Köthe spaces and finiteness spaces. We generalize the theory of Taylor expansion to models in which coefficients can be negative, and we prove that our generic web models always satisfy this new axiomatization. Therefore, all the aforementioned models feature a Taylor expansion.
Cite as
Christine Tasson and Aymeric Walch. Absolute Convergence and Taylor Expansion in Web Based Models of Linear Logic. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 29:1-29:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{tasson_et_al:LIPIcs.FSCD.2026.29,
author = {Tasson, Christine and Walch, Aymeric},
title = {{Absolute Convergence and Taylor Expansion in Web Based Models of Linear Logic}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {29:1--29:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.29},
URN = {urn:nbn:de:0030-drops-263794},
doi = {10.4230/LIPIcs.FSCD.2026.29},
annote = {Keywords: Categorical semantics, Linear Logic, Quantitative semantics, Taylor expansion}
}
Document
On the Consistency of Naive Set Theories over Substructural and Fuzzy Logics
Abstract
The purpose of this paper is to invite structural proof theorists to a challenging problem in substructural and fuzzy logics: the consistency of Cantor-Łukasiewicz naive set theory. To this end, we consider two logics: FLew (Full Lambek calculus with exchange and weakening) and its extension Ł (Lukasiewicz logic). The former is equivalent to !-free intuitionistic linear logic with weakening, while the latter is the most prominent system of mathematical fuzzy logic. For each of them, we consider two extensions: one with a fixed point operator (which is neither least nor greatest) and the other with a naive set theory with unrestricted comprehension, so that we end up with four systems: FLew_{fp}, FLew_{set}, Ł_{fp} and Ł_{set}. The first two admit an easy proof of consistency by cut elimination, while the third admits a proof by the Brouwer fixed point theorem. The last system Ł_{set} (known as Cantor-Łukasiewicz set theory) is our main target. Although there are some partial results, the consistency of the full system is still open. In this paper, we consider a restricted fragment of Ł_{set} and prove its consistency.
Cite as
Kazushige Terui. On the Consistency of Naive Set Theories over Substructural and Fuzzy Logics. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{terui:LIPIcs.FSCD.2026.30,
author = {Terui, Kazushige},
title = {{On the Consistency of Naive Set Theories over Substructural and Fuzzy Logics}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {30:1--30:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.30},
URN = {urn:nbn:de:0030-drops-263807},
doi = {10.4230/LIPIcs.FSCD.2026.30},
annote = {Keywords: substructural logics, mathematical fuzzy logics, fixed points, naive set theory}
}
Document
Type Theory with Erasure
Abstract
Erasure enriches type theory with a distinction between runtime relevant and irrelevant data, allowing the compilation step to safely erase the latter. Versions of this feature are implemented by many systems, including Agda, Idris, and Rocq. We present a structural version of type theory with erasure, formulated as a second-order generalised algebraic theory (SOGAT). Erasure is encoded as a phase distinction between runtime and erased terms, in the form of a proposition that can appear in a context. This formulation has several advantages: it has models based on categories with families, is compatible with other structural features such as staging, and provides a better guideline for implementation. Through the model theory of SOGATs, we study the semantics of type theory with erasure in families of sets, which generalises to any Grothendieck topos equipped with a tiny proposition. We establish conservativity over Martin-Löf type theory (MLTT) in both phases. For code extraction, we construct a presheaf model that produces untyped lambda calculus programs and prove its correctness through gluing. Our results are formalised in Agda and we provide a toy elaborator implementation.
Cite as
Constantine Theocharis and Edwin Brady. Type Theory with Erasure. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 31:1-31:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{theocharis_et_al:LIPIcs.FSCD.2026.31,
author = {Theocharis, Constantine and Brady, Edwin},
title = {{Type Theory with Erasure}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {31:1--31:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.31},
URN = {urn:nbn:de:0030-drops-263816},
doi = {10.4230/LIPIcs.FSCD.2026.31},
annote = {Keywords: Type theory, erasure, dependent types, compilation, synthetic phase distinction, higher-order abstract syntax, logical frameworks}
}
Document
New and Formalized Proofs for Right-Forward Closures and Core Matrix Interpretations
Abstract
We provide new proofs of two important theorems for proving termination of term rewrite systems (TRSs), including a full formalization in Isabelle/HOL.
We first consider Dershowitz' theorem that termination starting from arbitrary terms is equivalent to termination starting from terms in the right-forward closures of right-hand sides, provided that the TRS is right-linear or orthogonal. Our new proof deviates from the original one in that no reorderings of steps in infinite derivations are required, making it more precise in its argumentation. It also subsumes a later result that one can weaken orthogonality to locally confluent overlay TRSs.
The second theorem is about matrix interpretations. These were introduced by Hofbauer and Waldmann for proving termination of string rewrite systems (SRSs), internally using the concept of a core. Subsequently, Endrullis, Waldmann and Zantema developed matrix interpretations for TRSs without using the idea of a core. Whereas matrix interpretations for TRSs have already been formalized several times, so far this was not the case for core SRS matrix interpretations. We not only provide such a formalization, but also extend core SRS matrix interpretations to TRSs. These new core matrix interpretations for TRSs generalize previous approaches.
Cite as
René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, and Johannes Waldmann. New and Formalized Proofs for Right-Forward Closures and Core Matrix Interpretations. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{thiemann_et_al:LIPIcs.FSCD.2026.32,
author = {Thiemann, Ren\'{e} and Hofbauer, Dieter and Le Huitouze, Ulysse and Waldmann, Johannes},
title = {{New and Formalized Proofs for Right-Forward Closures and Core Matrix Interpretations}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {32:1--32:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.32},
URN = {urn:nbn:de:0030-drops-263825},
doi = {10.4230/LIPIcs.FSCD.2026.32},
annote = {Keywords: Isabelle/HOL, Matrix Interpretations, Narrowing, Right-Forward Closures, Term Rewriting}
}
Document
Investigations on Higher-Order Infinitary Logic
Abstract
Higher-order logic and infinitary logic are two extensions of first-order logic that allow greater expressivity. Both features have not been investigated together yet. In this paper, we define a higher-order infinitary logic, based on an extension of simple type theory. The resulting logic features higher-order quantifiers, infinite conjunctions and infinite disjunctions. We establish results at both the syntactic and the semantic level. We introduce a sound notion of model, and we show a strong version of completeness that entails the cut-elimination theorem for natural deduction. Moreover, we prove an extension of Barr’s theorem, allowing us to constructivize classical proofs of a particular fragment of higher-order infinitary logic.
Cite as
Thomas Traversié, Olivier Hermant, and Marc Aiguier. Investigations on Higher-Order Infinitary Logic. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 33:1-33:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{traversie_et_al:LIPIcs.FSCD.2026.33,
author = {Traversi\'{e}, Thomas and Hermant, Olivier and Aiguier, Marc},
title = {{Investigations on Higher-Order Infinitary Logic}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {33:1--33:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.33},
URN = {urn:nbn:de:0030-drops-263835},
doi = {10.4230/LIPIcs.FSCD.2026.33},
annote = {Keywords: Infinitary logic, higher-order logic, cut elimination, constructivization}
}
Document
Stabilized Profunctors and Matrix Representation
Abstract
The (bi)category of profunctors on groupoids is a categorification of the relational model of linear logic. Its objects are not just sets but rather sets whose elements are equipped with groups encoding their symmetries, and its morphisms carry actions by these symmetries. While detailed information on such symmetries helps with, e.g., adequacy proofs of profunctorial models, it makes operations such as composition more difficult to compute. A way to ease the computation is to transform a profunctor into a matrix. Although the matrix representation is not functorial in general, it is known to behave well for certain subclasses, such as the class of profunctors definable by λ-terms. The mathematical reason behind this phenomenon, however, was not understood.
This paper shows that the key is stability. Stability is a classical concept in domain theory, and has been extended to profunctors in Taylor’s work and further developed by Fiore et al. All λ-definable profunctors are known to be stabilized, and we show that the matrix representation behaves well for stabilized profunctors. We prove that the matrix representation defines a functor from stabilized profunctors to matrices that preserves the linear logic structures.
Cite as
Takeshi Tsukada, Kazuyuki Asada, and Kengo Hirata. Stabilized Profunctors and Matrix Representation. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 34:1-34:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{tsukada_et_al:LIPIcs.FSCD.2026.34,
author = {Tsukada, Takeshi and Asada, Kazuyuki and Hirata, Kengo},
title = {{Stabilized Profunctors and Matrix Representation}},
booktitle = {11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
pages = {34:1--34:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-433-8},
ISSN = {1868-8969},
year = {2026},
volume = {378},
editor = {Pfenning, Frank},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.34},
URN = {urn:nbn:de:0030-drops-263847},
doi = {10.4230/LIPIcs.FSCD.2026.34},
annote = {Keywords: Profunctor, weighted relational model, stability}
}