DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2026.38

The Biequivalence of Path Categories and Axiomatic Martin-Löf Type Theories

Authors: Daniël Otten and Matteo Spadetto

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract

The semantics of extensional type theory has an elegant categorical description: models of extensional =-types, 𝟙-types, and Σ-types are biequivalent to finitely complete categories, while adding Π-types yields locally Cartesian closed categories. We establish parallel results for axiomatic type theory, which includes systems like cubical type theory, where the computation rule of the =-types only holds as a propositional axiom instead of a definitional reduction. In particular, we prove that models of axiomatic =-types, and standard 𝟙- and Σ-types are biequivalent to certain path categories, while adding axiomatic Π-types yields dependent homotopy exponents. This biequivalence simplifies axiomatic =-types, which are more intricate than extensional ones since they permit higher dimensional structure. Specifically, path categories use a primitive notion of equivalence instead of a direct reproduction of the syntactic elimination rules and computation axioms. We apply our correspondence to prove a coherence theorem: we show that these weak homotopical models can be turned into equivalent strict models of axiomatic type theory. In addition, we introduce a more modular notion, that of a display map path category, which only models axiomatic =-types by default, while leaving room to add other axiomatic type formers such as 𝟙-, Σ-, and Π-types.

Cite as

Daniël Otten and Matteo Spadetto. The Biequivalence of Path Categories and Axiomatic Martin-Löf Type Theories. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 38:1-38:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{otten_et_al:LIPIcs.CSL.2026.38,
  author =	{Otten, Dani\"{e}l and Spadetto, Matteo},
  title =	{{The Biequivalence of Path Categories and Axiomatic Martin-L\"{o}f Type Theories}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{38:1--38:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.38},
  URN =		{urn:nbn:de:0030-drops-254633},
  doi =		{10.4230/LIPIcs.CSL.2026.38},
  annote =	{Keywords: Axiomatic type theory, cubical type theory, propositional equality, biequivalence, display map categories, path categories, homotopy theory, coherence}
}

Document

DOI: 10.4230/LIPIcs.CALCO.2025.10

EGGs Are Adhesive!

Authors: Roberto Biondo, Davide Castelnovo, and Fabio Gadducci

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract

The use of rewriting-based visual formalisms is on the rise. In the formal methods community, this is due also to the introduction of adhesive categories, where most properties of classical approaches to graph transformation, such as those on parallelism and confluence, can be rephrased and proved in a general and uniform way. E-graphs (EGGs) are a formalism for program optimisation via an efficient implementation of equality saturation. In short, EGGs can be defined as (acyclic) term graphs with an additional notion of equivalence on nodes that is closed under the operators of the signature. Instead of replacing the components of a program, the optimisation step is performed by adding new components and linking them to the existing ones via an equivalence relation, until an optimal program is reached. This work describes EGGs via adhesive categories. Besides the benefits in itself of a formal presentation, which renders precise the properties of the data structure, the description of the addition of equivalent program components using standard graph transformation tools offers the advantages of the adhesive framework in modelling, for example, concurrent updates.

Cite as

Roberto Biondo, Davide Castelnovo, and Fabio Gadducci. EGGs Are Adhesive!. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{biondo_et_al:LIPIcs.CALCO.2025.10,
  author =	{Biondo, Roberto and Castelnovo, Davide and Gadducci, Fabio},
  title =	{{EGGs Are Adhesive!}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{10:1--10:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.10},
  URN =		{urn:nbn:de:0030-drops-235690},
  doi =		{10.4230/LIPIcs.CALCO.2025.10},
  annote =	{Keywords: Hypergraphs, terms graphs, e-graphs, adhesive categories}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2025.33

Solving Guarded Domain Equations in Presheaves over Ordinals and Mechanizing It

Authors: Sergei Stepanenko and Amin Timany

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

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

DOI: 10.4230/LIPIcs.ECOOP.2025.12

Automatic Goal Clone Detection in Rocq

Authors: Ali Ghanbari

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract

Proof engineering in Rocq is a labor-intensive process, and as proof developments grow in size, redundancy and maintainability become challenges. One such redundancy is goal cloning, i.e., proving α-equivalent goals multiple times, leading to wasted effort and bloated proof scripts. In this paper, we introduce clone-finder, a novel technique for detecting goal clones in Rocq proofs. By leveraging the formal notion of α-equivalence for Gallina terms, clone-finder systematically identifies duplicated proof goals across large Rocq codebases. We evaluate clone-finder on 40 real-world Rocq projects from the CoqGym dataset. Our results reveal that each project contains an average of 27.73 instances of goal clone. We observed that the clones can be categorized as either exact goal duplication, generalization, or α-equivalent goals with different proofs, each signifying varying levels duplicate effort. Our findings highlight significant untapped potential for proof reuse in Rocq-based formal verification projects, paving the way for future improvements in automated proof engineering.

Cite as

Ali Ghanbari. Automatic Goal Clone Detection in Rocq. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ghanbari:LIPIcs.ECOOP.2025.12,
  author =	{Ghanbari, Ali},
  title =	{{Automatic Goal Clone Detection in Rocq}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{12:1--12:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.12},
  URN =		{urn:nbn:de:0030-drops-233055},
  doi =		{10.4230/LIPIcs.ECOOP.2025.12},
  annote =	{Keywords: Clone Detection, Goal, Proof, Rocq, Gallina}
}

Document

DOI: 10.4230/LIPIcs.CSL.2022.13

Fuzzy Algebraic Theories

Authors: Davide Castelnovo and Marino Miculan

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract

In this work we propose a formal system for fuzzy algebraic reasoning. The sequent calculus we define is based on two kinds of propositions, capturing equality and existence of terms as members of a fuzzy set. We provide a sound semantics for this calculus and show that there is a notion of free model for any theory in this system, allowing us (with some restrictions) to recover models as Eilenberg-Moore algebras for some monad. We will also prove a completeness result: a formula is derivable from a given theory if and only if it is satisfied by all models of the theory. Finally, leveraging results by Milius and Urbat, we give HSP-like characterizations of subcategories of algebras which are categories of models of particular kinds of theories.

Cite as

Davide Castelnovo and Marino Miculan. Fuzzy Algebraic Theories. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{castelnovo_et_al:LIPIcs.CSL.2022.13,
  author =	{Castelnovo, Davide and Miculan, Marino},
  title =	{{Fuzzy Algebraic Theories}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{13:1--13:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.13},
  URN =		{urn:nbn:de:0030-drops-157332},
  doi =		{10.4230/LIPIcs.CSL.2022.13},
  annote =	{Keywords: categorical logic, fuzzy sets, algebraic reasoning, equational axiomatisations, monads, Eilenberg-Moore algebras}
}

Document

DOI: 10.4230/LIPIcs.CALCO.2021.12

Closure Hyperdoctrines

Authors: Davide Castelnovo and Marino Miculan

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract

(Pre)closure spaces are a generalization of topological spaces covering also the notion of neighbourhood in discrete structures, widely used to model and reason about spatial aspects of distributed systems. In this paper we present an abstract theoretical framework for the systematic investigation of the logical aspects of closure spaces. To this end, we introduce the notion of closure (hyper)doctrines, i.e. doctrines endowed with inflationary operators (and subject to suitable conditions). The generality and effectiveness of this concept is witnessed by many examples arising naturally from topological spaces, fuzzy sets, algebraic structures, coalgebras, and covering at once also known cases such as Kripke frames and probabilistic frames (i.e., Markov chains). By leveraging general categorical constructions, we provide axiomatisations and sound and complete semantics for various fragments of logics for closure operators. Hence, closure hyperdoctrines are useful both for refining and improving the theory of existing spatial logics, and for the definition of new spatial logics for new applications.

Cite as

Davide Castelnovo and Marino Miculan. Closure Hyperdoctrines. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 12:1-12:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{castelnovo_et_al:LIPIcs.CALCO.2021.12,
  author =	{Castelnovo, Davide and Miculan, Marino},
  title =	{{Closure Hyperdoctrines}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{12:1--12:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.12},
  URN =		{urn:nbn:de:0030-drops-153678},
  doi =		{10.4230/LIPIcs.CALCO.2021.12},
  annote =	{Keywords: categorical logic, topological semantics, closure operators, spatial logic}
}

6 Search Results for "Miculan, Marino"

The Biequivalence of Path Categories and Axiomatic Martin-Löf Type Theories

Abstract

Cite as

EGGs Are Adhesive!

Abstract

Cite as

Solving Guarded Domain Equations in Presheaves over Ordinals and Mechanizing It

Abstract

Cite as

Automatic Goal Clone Detection in Rocq

Abstract

Cite as

Fuzzy Algebraic Theories

Abstract

Cite as

Closure Hyperdoctrines

Abstract

Cite as

Thanks for your feedback!

Could not send message