17 Search Results for "Mörtberg, Anders"

Document
DOI: 10.4230/LIPIcs.ITP.2025.14
Canonical for Automated Theorem Proving in Lean

Authors: Chase Norman and Jeremy Avigad

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Canonical is a solver for type inhabitation in dependent type theory, that is, the problem of producing a term of a given type. We present a Lean tactic which invokes Canonical to generate proof terms and synthesize programs. The tactic supports higher-order and dependently-typed goals, structural recursion over indexed inductive types, and definitional equality. Canonical finds proofs for 84% of Natural Number Game problems in 51 seconds total.
Cite as

Chase Norman and Jeremy Avigad. Canonical for Automated Theorem Proving in Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{norman_et_al:LIPIcs.ITP.2025.14,
  author =	{Norman, Chase and Avigad, Jeremy},
  title =	{{Canonical for Automated Theorem Proving in Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{14:1--14:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.14},
  URN =		{urn:nbn:de:0030-drops-246128},
  doi =		{10.4230/LIPIcs.ITP.2025.14},
  annote =	{Keywords: Automated Reasoning, Interactive Theorem Proving, Dependent Type Theory, Inhabitation, Unification, Program Synthesis, Formal Methods}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.20
Formalizing Colimits in 𝒞at

Authors: Mario Carneiro and Emily Riehl

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Certain results involving "higher structures" are not currently accessible to computer formalization because the prerequisite ∞-category theory has not been formalized. To support future work on formalizing ∞-category theory in Lean’s mathematics library, we formalize some fundamental constructions involving the 1-category of categories. Specifically, we construct the left adjoint to the nerve embedding of categories into simplicial sets, defining the homotopy category functor. We prove further that this adjunction is reflective, which allows us to conclude that 𝒞at has colimits. To our knowledge this is the first formalized proof that the nerve functor is a fully faithful right adjoint and that the category of categories is cocomplete.
Cite as

Mario Carneiro and Emily Riehl. Formalizing Colimits in 𝒞at. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{carneiro_et_al:LIPIcs.ITP.2025.20,
  author =	{Carneiro, Mario and Riehl, Emily},
  title =	{{Formalizing Colimits in 𝒞at}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{20:1--20:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.20},
  URN =		{urn:nbn:de:0030-drops-246186},
  doi =		{10.4230/LIPIcs.ITP.2025.20},
  annote =	{Keywords: category theory, infinity-category theory, nerve, simplicial set, colimit}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.17
Formalising Inductive and Coinductive Containers

Authors: Stefania Damato, Thorsten Altenkirch, and Axel Ljungström

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Containers capture the concept of strictly positive data types in programming. The original development of containers is done in the internal language of locally cartesian closed categories (LCCCs) with disjoint coproducts and W-types, and uniqueness of identity proofs (UIP) is implicitly assumed throughout. Although it is claimed that these developments can also be interpreted in extensional Martin-Löf type theory, this interpretation is not made explicit. In this paper, we present a formalisation of the results that "containers preserve least and greatest fixed points" in Cubical Agda, thereby giving a formulation in intensional type theory. Our proofs do not make use of UIP and thereby generalise the original results from talking about container functors on Set to container functors on the wild category of types. Our main incentive for using Cubical Agda is that its path type restores the equivalence between bisimulation and coinductive equality. Thus, besides developing container theory in a more general setting, we also demonstrate the usefulness of Cubical Agda’s path type to coinductive proofs.
Cite as

Stefania Damato, Thorsten Altenkirch, and Axel Ljungström. Formalising Inductive and Coinductive Containers. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{damato_et_al:LIPIcs.ITP.2025.17,
  author =	{Damato, Stefania and Altenkirch, Thorsten and Ljungstr\"{o}m, Axel},
  title =	{{Formalising Inductive and Coinductive Containers}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{17:1--17:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.17},
  URN =		{urn:nbn:de:0030-drops-246151},
  doi =		{10.4230/LIPIcs.ITP.2025.17},
  annote =	{Keywords: type theory, container, initial algebra, terminal coalgebra, Cubical Agda}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2025.4
Distributive Laws of Monadic Containers

Authors: Chris Purdy and Stefania Damato

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

Abstract
Containers are used to carve out a class of strictly positive data types in terms of shapes and positions. They can be interpreted via a fully-faithful functor into endofunctors on Set. Monadic containers are those containers whose interpretation as a Set functor carries a monad structure. The category of containers is closed under container composition and is a monoidal category, whereas monadic containers do not in general compose. In this paper, we develop a characterisation of distributive laws of monadic containers. Distributive laws were introduced as a sufficient condition for the composition of the underlying functors of two monads to also carry a monad structure. Our development parallels Ahman and Uustalu’s characterisation of distributive laws of directed containers, i.e. containers whose Set functor interpretation carries a comonad structure. Furthermore, by combining our work with theirs, we construct characterisations of mixed distributive laws (i.e. of directed containers over monadic containers and vice versa), thereby completing the "zoo" of container characterisations of (co)monads and their distributive laws. We have found these characterisations amenable to development of existence and uniqueness proofs of distributive laws, particularly in the mechanised setting of Cubical Agda, in which most of the theory of this paper has been formalised.
Cite as

Chris Purdy and Stefania Damato. Distributive Laws of Monadic Containers. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{purdy_et_al:LIPIcs.CALCO.2025.4,
  author =	{Purdy, Chris and Damato, Stefania},
  title =	{{Distributive Laws of Monadic Containers}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{4:1--4:22},
  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.4},
  URN =		{urn:nbn:de:0030-drops-235633},
  doi =		{10.4230/LIPIcs.CALCO.2025.4},
  annote =	{Keywords: distributive laws, monadic containers, monads, dependent types, cubical agda}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.30
Coherent Tietze Transformations of 1-Polygraphs in Homotopy Type Theory

Authors: Samuel Mimram and Émile Oleon

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

Abstract
Polygraphs play a fundamental role in algebra, geometry, and computer science, by generalizing group presentations to higher-dimensional structures and encoding coherence for those. They have recently been adapted by Kraus and von Raumer to the setting of homotopy type theory, where they are useful to define and study higher inductive types. Here, we develop the theory of 1-dimensional polygraphs, which correspond to presentations of sets in homotopy type theory. This requires us to introduce a dedicated notion of Tietze transformation, generalizing their well-known counterpart in group theory: the equivalence generated by those transformations characterizes situations where two 1-polygraphs present the same set. We also show a homotopy transfer theorem, which provides a way to transport coherence structures from one 1-polygraph to another. This work lays the foundations for a general theory of polygraphs in arbitrary dimensions, which should be useful for instance to define and study coherent group presentations, allowing for synthetic (co)homology computations. Most of the results in the article have been formalized with the Agda proof assistant using the cubical HoTT library.
Cite as

Samuel Mimram and Émile Oleon. Coherent Tietze Transformations of 1-Polygraphs in Homotopy Type Theory. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{mimram_et_al:LIPIcs.FSCD.2025.30,
  author =	{Mimram, Samuel and Oleon, \'{E}mile},
  title =	{{Coherent Tietze Transformations of 1-Polygraphs in Homotopy Type Theory}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{30:1--30:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.30},
  URN =		{urn:nbn:de:0030-drops-236456},
  doi =		{10.4230/LIPIcs.FSCD.2025.30},
  annote =	{Keywords: homotopy type theory, polygraph, Tietze transformation, coherence}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.27
What Does It Take to Certify a Conversion Checker?

Authors: Meven Lennon-Bertrand

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

Abstract
We report on a detailed exploration of the properties of conversion (definitional equality) in dependent type theory, with the goal of certifying decision procedures for it. While in that context the property of normalisation has attracted the most light, we instead emphasize the importance of injectivity properties, showing that they alone are both crucial and sufficient to certify most desirable properties of conversion checkers. We also explore the certification of a fully untyped conversion checker, with respect to a typed specification, and show that the story is mostly unchanged, although the exact injectivity properties needed are subtly different.
Cite as

Meven Lennon-Bertrand. What Does It Take to Certify a Conversion Checker?. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lennonbertrand:LIPIcs.FSCD.2025.27,
  author =	{Lennon-Bertrand, Meven},
  title =	{{What Does It Take to Certify a Conversion Checker?}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{27:1--27:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.27},
  URN =		{urn:nbn:de:0030-drops-236428},
  doi =		{10.4230/LIPIcs.FSCD.2025.27},
  annote =	{Keywords: Dependent types, Bidirectional typing, Certified software}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2024.9
Complexity of Cubical Cofibration Logics I: coNP-Complete Examples

Authors: Robert Rose and Daniel R. Licata

Published in: LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024)

Abstract
We provide a comprehensive classification of the cofibration entailment problem, COFENT, for the cofibration logics of various cubical type theories in use today. The problem COFENT arose from the need of cubical proof assistants to automate reasoning about cubical complexes included in an n-dimensional hypercube. Intuitively, it asks: given logical descriptions of two such complexes, is one a subcomplex of the other? We show that the common variants of COFENT are coNP-complete.
Cite as

Robert Rose and Daniel R. Licata. Complexity of Cubical Cofibration Logics I: coNP-Complete Examples. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{rose_et_al:LIPIcs.TYPES.2024.9,
  author =	{Rose, Robert and Licata, Daniel R.},
  title =	{{Complexity of Cubical Cofibration Logics I: coNP-Complete Examples}},
  booktitle =	{30th International Conference on Types for Proofs and Programs (TYPES 2024)},
  pages =	{9:1--9:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-376-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{336},
  editor =	{M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.9},
  URN =		{urn:nbn:de:0030-drops-233711},
  doi =		{10.4230/LIPIcs.TYPES.2024.9},
  annote =	{Keywords: cubical sets, internal language, intuitionistic logic, dependent type theory, homotopy type theory, decision procedures}
}
Document
DOI: 10.4230/OASIcs.FMBC.2025.11
Formally Specifying Contract Optimizations with Bisimulations in Coq

Authors: Derek Sorensen

Published in: OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025)

Abstract
The efficacy of formal verification of smart contracts depends on being able to correctly specify and carry out the verification of optimized code. However, code optimized for performance is rarely optimized for intelligibility, which can make formally verifying optimized code difficult and costly. To address this issue, we present a formal tool for reasoning about an optimized contract in terms of its reference implementation. This tool reduces the work of formally verifying an optimized contract to proving behavioral equivalence to the reference implementation.
Cite as

Derek Sorensen. Formally Specifying Contract Optimizations with Bisimulations in Coq. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 11:1-11:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{sorensen:OASIcs.FMBC.2025.11,
  author =	{Sorensen, Derek},
  title =	{{Formally Specifying Contract Optimizations with Bisimulations in Coq}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{11:1--11:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-371-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{129},
  editor =	{Marmsoler, Diego and Xu, Meng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.11},
  URN =		{urn:nbn:de:0030-drops-230382},
  doi =		{10.4230/OASIcs.FMBC.2025.11},
  annote =	{Keywords: smart contract verification, formal methods, interactive theorem prover, smart contract upgradeability}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.38
The Functor of Points Approach to Schemes in Cubical Agda

Authors: Max Zeuner and Matthias Hutzler

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
We present a formalization of quasi-compact and quasi-separated schemes (qcqs-schemes) in the Cubical Agda proof assistant. We follow Grothendieck’s functor of points approach, which defines schemes, the quintessential notion of modern algebraic geometry, as certain well-behaved functors from commutative rings to sets. This approach is often regarded as conceptually simpler than the standard approach of defining schemes as locally ringed spaces, but to our knowledge it has not yet been adopted in formalizations of algebraic geometry. We build upon a previous formalization of the so-called Zariski lattice associated to a commutative ring in order to define the notion of compact open subfunctor. This allows for a concise definition of qcqs-schemes, streamlining the usual presentation as e.g. given in the standard textbook of Demazure and Gabriel. It also lets us obtain a fully constructive proof that compact open subfunctors of affine schemes are qcqs-schemes.
Cite as

Max Zeuner and Matthias Hutzler. The Functor of Points Approach to Schemes in Cubical Agda. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 38:1-38:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{zeuner_et_al:LIPIcs.ITP.2024.38,
  author =	{Zeuner, Max and Hutzler, Matthias},
  title =	{{The Functor of Points Approach to Schemes in Cubical Agda}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{38:1--38:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.38},
  URN =		{urn:nbn:de:0030-drops-207667},
  doi =		{10.4230/LIPIcs.ITP.2024.38},
  annote =	{Keywords: Schemes, Algebraic Geometry, Category Theory, Cubical Agda, Homotopy Type Theory and Univalent Foundations, Constructive Mathematics}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.22
Automating Boundary Filling in Cubical Agda

Authors: Maximilian Doré, Evan Cavallo, and Anders Mörtberg

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
When working in a proof assistant, automation is key to discharging routine proof goals such as equations between algebraic expressions. Homotopy Type Theory allows the user to reason about higher structures, such as topological spaces, using higher inductive types (HITs) and univalence. Cubical Agda is an extension of Agda with computational support for HITs and univalence. A difficulty when working in Cubical Agda is dealing with the complex combinatorics of higher structures, an infinite-dimensional generalisation of equational reasoning. To solve these higher-dimensional equations consists in constructing cubes with specified boundaries. We develop a simplified cubical language in which we isolate and study two automation problems: contortion solving, where we attempt to "contort" a cube to fit a given boundary, and the more general Kan solving, where we search for solutions that involve pasting multiple cubes together. Both problems are difficult in the general case - Kan solving is even undecidable - so we focus on heuristics that perform well on practical examples. We provide a solver for the contortion problem using a reformulation of contortions in terms of poset maps, while we solve Kan problems using constraint satisfaction programming. We have implemented our algorithms in an experimental Haskell solver that can be used to automatically solve goals presented by Cubical Agda. We illustrate this with a case study establishing the Eckmann-Hilton theorem using our solver, as well as various benchmarks - providing the ground for further study of proof automation in cubical type theories.
Cite as

Maximilian Doré, Evan Cavallo, and Anders Mörtberg. Automating Boundary Filling in Cubical Agda. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{dore_et_al:LIPIcs.FSCD.2024.22,
  author =	{Dor\'{e}, Maximilian and Cavallo, Evan and M\"{o}rtberg, Anders},
  title =	{{Automating Boundary Filling in Cubical Agda}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{22:1--22:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.22},
  URN =		{urn:nbn:de:0030-drops-203514},
  doi =		{10.4230/LIPIcs.FSCD.2024.22},
  annote =	{Keywords: Cubical Agda, Automated Reasoning, Constraint Satisfaction Programming}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2022.14
A Univalent Formalization of Constructive Affine Schemes

Authors: Max Zeuner and Anders Mörtberg

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract
We present a formalization of constructive affine schemes in the Cubical Agda proof assistant. This development is not only fully constructive and predicative, it also makes crucial use of univalence. By now schemes have been formalized in various proof assistants. However, most existing formalizations follow the inherently non-constructive approach of Hartshorne’s classic "Algebraic Geometry" textbook, for which the construction of the so-called structure sheaf is rather straightforwardly formalizable and works the same with or without univalence. We follow an alternative approach that uses a point-free description of the constructive counterpart of the Zariski spectrum called the Zariski lattice and proceeds by defining the structure sheaf on formal basic opens and then lift it to the whole lattice. This general strategy is used in a plethora of textbooks, but formalizing it has proved tricky. The main result of this paper is that with the help of the univalence principle we can make this "lift from basis" strategy formal and obtain a fully formalized account of constructive affine schemes.
Cite as

Max Zeuner and Anders Mörtberg. A Univalent Formalization of Constructive Affine Schemes. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 14:1-14:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{zeuner_et_al:LIPIcs.TYPES.2022.14,
  author =	{Zeuner, Max and M\"{o}rtberg, Anders},
  title =	{{A Univalent Formalization of Constructive Affine Schemes}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{14:1--14:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.14},
  URN =		{urn:nbn:de:0030-drops-184574},
  doi =		{10.4230/LIPIcs.TYPES.2022.14},
  annote =	{Keywords: Affine Schemes, Homotopy Type Theory and Univalent Foundations, Cubical Agda, Constructive Mathematics}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.11
Synthetic Integral Cohomology in Cubical Agda

Authors: Guillaume Brunerie, Axel Ljungström, and Anders Mörtberg

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

Abstract
This paper discusses the formalization of synthetic cohomology theory in a cubical extension of Agda which natively supports univalence and higher inductive types. This enables significant simplifications of many proofs from Homotopy Type Theory and Univalent Foundations as steps that used to require long calculations now hold simply by computation. To this end, we give a new definition of the group structure for cohomology with ℤ-coefficients, optimized for efficient computations. We also invent an optimized definition of the cup product which allows us to give the first complete formalization of the axioms needed to turn the integral cohomology groups into a graded commutative ring. Using this, we characterize the cohomology groups of the spheres, torus, Klein bottle and real/complex projective planes. As all proofs are constructive we can then use Cubical Agda to distinguish between spaces by computation.
Cite as

Guillaume Brunerie, Axel Ljungström, and Anders Mörtberg. Synthetic Integral Cohomology in Cubical Agda. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{brunerie_et_al:LIPIcs.CSL.2022.11,
  author =	{Brunerie, Guillaume and Ljungstr\"{o}m, Axel and M\"{o}rtberg, Anders},
  title =	{{Synthetic Integral Cohomology in Cubical Agda}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{11:1--11:19},
  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.11},
  URN =		{urn:nbn:de:0030-drops-157310},
  doi =		{10.4230/LIPIcs.CSL.2022.11},
  annote =	{Keywords: Synthetic Homotopy Theory, Cohomology Theory, Cubical Agda}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2019.10
Higher Inductive Type Eliminators Without Paths

Authors: Nils Anders Danielsson

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)

Abstract
Cubical Agda has support for higher inductive types. Paths are integral to the working of this feature. However, there are other notions of equality. For instance, Cubical Agda comes with an identity type family for which the J rule computes in the usual way when applied to the canonical proof of reflexivity, whereas typical implementations of the J rule for paths do not. This text shows how one can use some of the higher inductive types definable in Cubical Agda with arbitrary notions of equality satisfying certain axioms. The method works for several examples taken from the HoTT book, including the interval, the circle, suspensions, pushouts, the propositional truncation, a general truncation operator, and set quotients.
Cite as

Nils Anders Danielsson. Higher Inductive Type Eliminators Without Paths. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{danielsson:LIPIcs.TYPES.2019.10,
  author =	{Danielsson, Nils Anders},
  title =	{{Higher Inductive Type Eliminators Without Paths}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{10:1--10:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.10},
  URN =		{urn:nbn:de:0030-drops-130749},
  doi =		{10.4230/LIPIcs.TYPES.2019.10},
  annote =	{Keywords: Cubical Agda, higher inductive types}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.13
Internal Parametricity for Cubical Type Theory

Authors: Evan Cavallo and Robert Harper

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic functions between higher inductive types, and we give an account of the identity extension lemma for internal parametricity.
Cite as

Evan Cavallo and Robert Harper. Internal Parametricity for Cubical Type Theory. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cavallo_et_al:LIPIcs.CSL.2020.13,
  author =	{Cavallo, Evan and Harper, Robert},
  title =	{{Internal Parametricity for Cubical Type Theory}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{13:1--13:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.13},
  URN =		{urn:nbn:de:0030-drops-116564},
  doi =		{10.4230/LIPIcs.CSL.2020.13},
  annote =	{Keywords: parametricity, cubical type theory, higher inductive types}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.14
Unifying Cubical Models of Univalent Type Theory

Authors: Evan Cavallo, Anders Mörtberg, and Andrew W Swan

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
We present a new constructive model of univalent type theory based on cubical sets. Unlike prior work on cubical models, ours depends neither on diagonal cofibrations nor connections. This is made possible by weakening the notion of fibration from the cartesian cubical set model, so that it is not necessary to assume that the diagonal on the interval is a cofibration. We have formally verified in Agda that these fibrations are closed under the type formers of cubical type theory and that the model satisfies the univalence axiom. By applying the construction in the presence of diagonal cofibrations or connections and reversals, we recover the existing cartesian and De Morgan cubical set models as special cases. Generalizing earlier work of Sattler for cubical sets with connections, we also obtain a Quillen model structure.
Cite as

Evan Cavallo, Anders Mörtberg, and Andrew W Swan. Unifying Cubical Models of Univalent Type Theory. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cavallo_et_al:LIPIcs.CSL.2020.14,
  author =	{Cavallo, Evan and M\"{o}rtberg, Anders and Swan, Andrew W},
  title =	{{Unifying Cubical Models of Univalent Type Theory}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{14:1--14:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.14},
  URN =		{urn:nbn:de:0030-drops-116578},
  doi =		{10.4230/LIPIcs.CSL.2020.14},
  annote =	{Keywords: Cubical Set Models, Cubical Type Theory, Homotopy Type Theory, Univalent Foundations}
}
  • Refine by Type
  • 17 Document/PDF
  • 7 Document/HTML

  • Refine by Publication Year
  • 8 2025
  • 2 2024
  • 1 2023
  • 1 2022
  • 3 2020
  • Show More...

  • Refine by Author
  • 5 Mörtberg, Anders
  • 3 Cavallo, Evan
  • 2 Damato, Stefania
  • 2 Ljungström, Axel
  • 2 Zeuner, Max
  • Show More...

  • Refine by Series/Journal
  • 16 LIPIcs
  • 1 OASIcs

  • Refine by Classification
  • 12 Theory of computation → Type theory
  • 5 Theory of computation → Constructive mathematics
  • 4 Theory of computation → Logic and verification
  • 2 Theory of computation → Automated reasoning
  • 2 Theory of computation → Type structures
  • Show More...

  • Refine by Keyword
  • 6 Cubical Agda
  • 2 Automated Reasoning
  • 2 Constructive Mathematics
  • 2 Homotopy Type Theory and Univalent Foundations
  • 2 cubical sets
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact