Computational Synthetic Cohomology Theory in Homotopy Type Theory
Mathematical Structures in Computer Science, 2025
Axel Ljungström, Anders Mörtberg
Available here
Publications and preprints
Formalising inductive and coinductive containers
To appear at ITP 2025
Stefania Damato, Thorsten Altenkirch, Axel Ljungström
Arxiv
The Steenrod squares via unordered joins
To appear in Proceedings of LICS 2025
Axel Ljungström, David Wärn
Arxiv
Distinguished Paper Award (LICS 2025)
Kleene Award (LICS 2025)
Cellular Methods in Homotopy Type Theory
Preprint, 2025
Axel Ljungström, Loïc Pujet
Available here
Symmetric Monoidal Smash Products in Homotopy Type Theory
Mathematical Structures in Computer Science, 2024
Axel Ljungström
Available here
Preprint version awarded best student paper (HoTT 2023)
Formalising and Computing the Fourth Homotopy Group of the 3-Sphere in Cubical Agda
Submitted, 2023
Axel Ljungström, Anders Mörtberg
Arxiv
Extended version of `Formalizing π₄(S³) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda’
Formalizing π₄(S³) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda
Proceedings of LICS 2023
Axel Ljungström, Anders Mörtberg
Arxiv
Distinguished Paper Award (LICS 2023)
Computing Cohomology Rings in Cubical Agda
Proceedings of CPP 2023
Thomas Lamiaux, Axel Ljungström, Anders Mörtberg
Arxiv
Distinguished Paper Award (CPP 2023)
Synethetic Integral Cohomology in Cubical Agda
Proceedings of CSL 2022
Guillaume Brunerie, Axel Ljungström, Anders Mörtberg
Available here