10 Search Results for "Ljungström, Axel"

Artifact
Software
DOI: 10.4230/artifacts.26875
Cellular Methods in Homotopy Type Theory (accompanying formalisation)

Authors: Axel Ljungström and Loïc Pujet

Abstract
Cite as

Axel Ljungström, Loïc Pujet. Cellular Methods in Homotopy Type Theory (accompanying formalisation) (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26875,
   title = {{Cellular Methods in Homotopy Type Theory (accompanying formalisation)}}, 
   author = {Ljungstr\"{o}m, Axel and Pujet, Lo\"{i}c},
   note = {Software, Knut and Alice Wallenberg Foundation Postdoctoral Scholarship: Program in Mathematics for researchers with a Swedish doctor’s degree, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:7904cf81046d351ce2a27f778d8b96f71186035d;origin=https://github.com/agda/cubical;visit=swh:1:snp:82843e2d41d4b8b6a9013ffeadeb01fbcbb23e53;anchor=swh:1:rev:8a45d739ad0b75f4773874be4a5e42dbd46c9cd6}{\texttt{swh:1:dir:7904cf81046d351ce2a27f778d8b96f71186035d}} (visited on 2026-07-09)},
   url = {https://github.com/agda/cubical/blob/master/Cubical/Papers/CellularMethods.agda},
   doi = {10.4230/artifacts.26875},
}
Artifact
Software
DOI: 10.4230/artifacts.26876
A Computer Formalisation of the Serre Finiteness Theorem (accompanying formalisation)

Authors: Reid Barton, Axel Ljungström, Owen Milner, and Anders Mörtberg

Abstract
Cite as

Reid Barton, Axel Ljungström, Owen Milner, Anders Mörtberg. A Computer Formalisation of the Serre Finiteness Theorem (accompanying formalisation) (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{SerreFiniteness,
   title = {{A Computer Formalisation of the Serre Finiteness Theorem (accompanying formalisation)}}, 
   author = {Barton, Reid and Ljungstr\"{o}m, Axel and Milner, Owen and M\"{o}rtberg, Anders},
   note = {Software, ForCUTT project, ERC advanced grant 101053291, Knut & Alice Wallenberg Foundation’s Program for Mathematics, This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0009, PI Steve Awodey, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:5c9314da89014673a22878132bb63cfc42ccfa73;origin=https://github.com/CMU-HoTT/serre-finiteness;visit=swh:1:snp:0f3bfe0f67361dc33562f0fc15b80309b3290611;anchor=swh:1:rev:79f3150942a129eb544004adcdef4b17244d5ed4}{\texttt{swh:1:dir:5c9314da89014673a22878132bb63cfc42ccfa73}} (visited on 2026-07-09)},
   url = {https://github.com/CMU-HoTT/serre-finiteness},
   doi = {10.4230/artifacts.26876},
}
Document
DOI: 10.4230/LIPIcs.LICS.2026.16
A Computer Formalisation of the Serre Finiteness Theorem

Authors: Reid Barton, Axel Ljungström, Owen Milner, and Anders Mörtberg

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
Few constructions in mathematics are as elusive as the homotopy groups of spheres. These groups, which intuitively measure n-dimensional loops on m-dimensional spheres, appear at first glance to be almost completely random - an unfortunate fact, seeing as they constitute one of the fundamental building blocks of algebraic topology and homotopy theory. However, the situation is not completely hopeless: in 1951, Serre proved his celebrated finiteness theorem, which says that these groups are almost always finite abelian groups, except in two classes of special cases when they also contain copies of the integers. In a recent paper, Barton and Campion proved a variation of this result in homotopy type theory (HoTT) - an extension of Martin-Löf type theory, particularly suitable for reasoning about and formalising algebraic topology and homotopy theory. Their result shows that the homotopy groups of spheres are all finitely presented - and constructively so. Prior to this proof, only low-dimensional homotopy groups of spheres had been computed in HoTT. This made it a major breakthrough for HoTT as a foundation and, as such, the immediate target of a full-scale formalisation project. In this paper, we present the outcome of this project: a complete formalisation of Barton and Campion’s proof of the Serre finiteness theorem in Cubical Agda, a constructive proof assistant implementing a cubical flavour of HoTT. In the light of the constructivity of Cubical Agda, we discuss the prospect of running the algorithm provided by our formalisation in order to compute concrete homotopy groups of spheres.
Cite as

Reid Barton, Axel Ljungström, Owen Milner, and Anders Mörtberg. A Computer Formalisation of the Serre Finiteness Theorem. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 16:1-16:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{barton_et_al:LIPIcs.LICS.2026.16,
  author =	{Barton, Reid and Ljungstr\"{o}m, Axel and Milner, Owen and M\"{o}rtberg, Anders},
  title =	{{A Computer Formalisation of the Serre Finiteness Theorem}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{16:1--16:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.16},
  URN =		{urn:nbn:de:0030-drops-268031},
  doi =		{10.4230/LIPIcs.LICS.2026.16},
  annote =	{Keywords: Homotopy type theory, synthetic homotopy theory, formalisation of mathematics, constructive mathematics}
}
Document
DOI: 10.4230/LIPIcs.LICS.2026.66
Cellular Methods in Homotopy Type Theory

Authors: Axel Ljungström and Loïc Pujet

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
In classical mathematics, a CW complex is a topological space which can be built up inductively by gluing together cells of increasing dimension. Thanks to their excellent categorical properties, CW complexes have become one of the main objects of interest in algebraic topology. Although their quasi-combinatorial nature suggests that a constructive treatment is possible, there seems to be little literature on the subject - perhaps because of the important role played by the axiom of choice in the classical theory of CW complexes. In this paper, we present a synthetic and constructive account of the theory of CW complexes in homotopy type theory. Our first main result is a finitary version of the cellular approximation theorem which, among other things, allows us to construct a cellular homology functor without needing the axiom of choice or relying on a pre-existing notion of homology. Our second main result, which we call the "Hurewicz approximation theorem", shows that the CW complexes that are n-connected types are precisely the ones that can be presented by a CW structure with no nontrivial cells up to dimension n. This theorem is standard in the classical treatment of CW complexes, but it is far from being obvious in a constructive setting. As a corollary, we give a new proof of the Hurewicz theorem for CW complexes, which relates the first non-vanishing homotopy group of a CW complex with the corresponding homology group. All key theorems presented in this paper have been mechanised in Cubical Agda.
Cite as

Axel Ljungström and Loïc Pujet. Cellular Methods in Homotopy Type Theory. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 66:1-66:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ljungstrom_et_al:LIPIcs.LICS.2026.66,
  author =	{Ljungstr\"{o}m, Axel and Pujet, Lo\"{i}c},
  title =	{{Cellular Methods in Homotopy Type Theory}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{66:1--66:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.66},
  URN =		{urn:nbn:de:0030-drops-268536},
  doi =		{10.4230/LIPIcs.LICS.2026.66},
  annote =	{Keywords: Homotopy type theory, Univalent foundations, constructive mathematics, synthetic homotopy theory, CW complexes, cellular homology, Hurewicz theorem}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.20
On Left Adjoints Preserving Colimits in HoTT

Authors: Perry Hart

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

Abstract
We examine how the standard proof that left adjoints preserve colimits behaves in the setting of wild categories, a natural setting for synthetic homotopy theory inside homotopy type theory. We prove that the proof may fail for adjunctions between wild categories. Our core contribution, however, is a sufficient condition on the left adjoint for the proof to go through. The condition, called 2-coherence, expresses that the naturality structure of the hom-isomorphism commutes with composition of morphisms. We present two useful examples of this condition in action. First, we use it, along with a new version of a known trick for homogeneous types, to show that the suspension functor preserves graph-indexed colimits. Second, we show that every modality, viewed as a functor on coslices of a type universe, is 2-coherent as a left adjoint to the forgetful functor from the subcategory of modal types, thereby proving this subcategory is cocomplete. We have formalized our main results in Agda.
Cite as

Perry Hart. On Left Adjoints Preserving Colimits in HoTT. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 20:1-20:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{hart:LIPIcs.CSL.2026.20,
  author =	{Hart, Perry},
  title =	{{On Left Adjoints Preserving Colimits in HoTT}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{20:1--20:17},
  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.20},
  URN =		{urn:nbn:de:0030-drops-254442},
  doi =		{10.4230/LIPIcs.CSL.2026.20},
  annote =	{Keywords: wild categories, colimits, adjunctions, homotopy type theory, category theory, synthetic homotopy theory, higher inductive types, modalities}
}
Artifact
Software
DOI: 10.4230/artifacts.24710
stefaniatadama/formalising-inductive-coinductive-containers

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

Abstract
Cite as

Stefania Damato, Thorsten Altenkirch, Axel Ljungström. stefaniatadama/formalising-inductive-coinductive-containers (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-24710,
   title = {{stefaniatadama/formalising-inductive-coinductive-containers}}, 
   author = {Damato, Stefania and Altenkirch, Thorsten and Ljungstr\"{o}m, Axel},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:a75b7ddaa46ca9a9f3ee6f65d22ba3b1c959d6d4;origin=https://github.com/stefaniatadama/formalising-inductive-coinductive-containers;visit=swh:1:snp:eebf2acbd002c4877bc6057e65e8ddef2b0fe79e;anchor=swh:1:rev:4e587677bdc0c7cb793ad8612c1e6e88c16877e7}{\texttt{swh:1:dir:a75b7ddaa46ca9a9f3ee6f65d22ba3b1c959d6d4}} (visited on 2025-09-22)},
   url = {https://github.com/stefaniatadama/formalising-inductive-coinductive-containers/blob/main/cubical/Cubical/Papers/Containers.agda},
   doi = {10.4230/artifacts.24710},
}
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.WABI.2025.11
Mutational Signature Refitting on Sparse Pan-Cancer Data

Authors: Gal Gilad, Teresa M. Przytycka, and Roded Sharan

Published in: LIPIcs, Volume 344, 25th International Conference on Algorithms for Bioinformatics (WABI 2025)

Abstract
Mutational processes shape cancer genomes, leaving characteristic marks that are termed signatures. The level of activity of each such process, or its signature exposure, provides important information on the disease, improving patient stratification and the prediction of drug response. Thus, there is growing interest in developing refitting methods that decipher those exposures. Previous work in this domain was unsupervised in nature, employing algebraic decomposition and probabilistic inference methods. Here we provide a supervised approach to the problem of signature refitting and show its superiority over current methods. Our method, SuRe, leverages a neural network model to capture correlations between signature exposures in real data. We show that SuRe outperforms previous methods on sparse mutation data from tumor type specific data sets, as well as pan-cancer data sets, with an increasing advantage as the data become sparser. We further demonstrate its utility in clinical settings.
Cite as

Gal Gilad, Teresa M. Przytycka, and Roded Sharan. Mutational Signature Refitting on Sparse Pan-Cancer Data. In 25th International Conference on Algorithms for Bioinformatics (WABI 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 344, pp. 11:1-11:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gilad_et_al:LIPIcs.WABI.2025.11,
  author =	{Gilad, Gal and Przytycka, Teresa M. and Sharan, Roded},
  title =	{{Mutational Signature Refitting on Sparse Pan-Cancer Data}},
  booktitle =	{25th International Conference on Algorithms for Bioinformatics (WABI 2025)},
  pages =	{11:1--11:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-386-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{344},
  editor =	{Brejov\'{a}, Bro\v{n}a and Patro, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.WABI.2025.11},
  URN =		{urn:nbn:de:0030-drops-239374},
  doi =		{10.4230/LIPIcs.WABI.2025.11},
  annote =	{Keywords: mutational signatures, signature refitting, cancer genomics, genomic data analysis, somatic mutations}
}
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.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}
}
  • Refine by Type
  • 7 Document/PDF
  • 3 Artifact
  • 2 Document/HTML

  • Refine by Publication Year
  • 5 2026
  • 3 2025
  • 1 2024
  • 1 2022

  • Refine by Author
  • 7 Ljungström, Axel
  • 4 Mörtberg, Anders
  • 2 Altenkirch, Thorsten
  • 2 Barton, Reid
  • 2 Damato, Stefania
  • Show More...

  • Refine by Series/Journal
  • 7 LIPIcs

  • Refine by Classification
  • 6 Theory of computation → Type theory
  • 2 Theory of computation → Constructive mathematics
  • 1 Applied computing → Bioinformatics
  • 1 Computing methodologies → Theorem proving algorithms
  • 1 Theory of computation → Automated reasoning
  • Show More...

  • Refine by Keyword
  • 3 Cubical Agda
  • 3 synthetic homotopy theory
  • 2 Homotopy type theory
  • 2 constructive mathematics
  • 1 Automated Reasoning
  • 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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact