Publications

Sometimes I forget to update this page, then please see my Google scholar page.

Papers

  1. Automating Boundary Filling in Cubical Agda - Maximilian Doré, Evan Cavallo, Anders Mörtberg. Preprint 2024.
  2. The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations - Daniel Gratzer, Håkon Gylterud, Anders Mörtberg, Elisabeth Stenholm. Preprint 2024.
  3. Computational Synthetic Cohomology Theory in Homotopy Type Theory - Axel Ljungström and Anders Mörtberg. Preprint 2024.
  4. Formalizing π4(S3)≅Z/2Z and Computing a Brunerie Number in Cubical Agda - Axel Ljungström and Anders Mörtberg. In the proceedings of LICS 2023. Distinguished Paper Award.
  5. Computing Cohomology Rings in Cubical Agda - Thomas Lamiaux, Axel Ljungström, Anders Mörtberg. In the proceedings of CPP 2023. Distinguished Paper Award.
  6. A Univalent Formalization of Constructive Affine Schemes - Max Zeuner and Anders Mörtberg. In the proceedings of TYPES 2022.
  7. Implementing a Category-Theoretic Framework for Typed Abstract Syntax - Benedikt Ahrens, Ralph Matthes, Anders Mörtberg. In the proceedings of CPP 2022.
  8. Synthetic Integral Cohomology in Cubical Agda - Guillaume Brunerie, Axel Ljungström, Anders Mörtberg. In the proceedings of CSL 2022.
  9. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types - Andrea Vezzosi, Anders Mörtberg, Andreas Abel. In Journal of Functional Programming, 2021. Extended version of ICFP paper with same title.
  10. Internalizing Representation Independence with Univalence - Carlo Angiuli, Evan Cavallo, Anders Mörtberg, Max Zeuner. In the proceedings of POPL 2021.
  11. Cubical Methods in Homotopy Type Theory and Univalent Foundations - Anders Mörtberg. In Mathematical Structures in Computer Science, 2021. Lecture notes for the 2019 HoTT Summer School
  12. Cubical Synthetic Homotopy Theory - Anders Mörtberg, Loïc Pujet. In the proceedings of CPP 2020.
  13. Unifying Cubical Models of Univalent Type Theory - Evan Cavallo, Anders Mörtberg, Andrew W Swan. In the proceedings of CSL 2020.
  14. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types - Andrea Vezzosi, Anders Mörtberg, Andreas Abel. In the proceedings of ICFP 2019. Distinguished Paper Award.
  15. On Higher Inductive Types in Cubical Type Theory - Thierry Coquand, Simon Huber and Anders Mörtberg. In the proceedings of LICS 2018.
  16. Cubical Type Theory a constructive interpretation of the univalence axiom - Cyril Cohen, Thierry Coquand, Simon Huber and Anders Mörtberg. In the proceedings of IfCoLog Journal of Logics and their Applications 2017. Slightly extended version of the paper on cubical type theory using the "forward" operation for propositional truncation (which simplifies the presentation of its composition operation).
  17. From signatures to monads in UniMath - Benedikt Ahrens, Ralph Matthes and Anders Mörtberg. In Journal of Automated Reasoning, 2019. Part of Special Issue on Homotopy Type Theory and Univalent Foundations.
  18. Some Wellfounded Trees in UniMath - Benedikt Ahrens and Anders Mörtberg. In the proceedings of ICMS 2016.
  19. Formalized Linear Algebra over Elementary Divisor Rings in Coq - Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg and Vincent Siles. In Logical Methods in Computer Science, 2016.
  20. Cubical Type Theory a constructive interpretation of the univalence axiom - Cyril Cohen, Thierry Coquand, Simon Huber and Anders Mörtberg. In the proceedings of TYPES 2015.
  21. A Coq Formalization of Finitely Presented Modules - Cyril Cohen and Anders Mörtberg. In the proceedings of ITP 2014.
  22. Computing Persistent Homology within Coq/SSReflect - Jónathan Heras, Thierry Coquand, Anders Mörtberg and Vincent Siles. In ACM Transactions on Computational Logic, 2013.
  23. Refinements for free! - Cyril Cohen, Maxime Dénès and Anders Mörtberg. In the proceedings of CPP 2013.
  24. Coherent and Strongly Discrete Rings in Type Theory - Thierry Coquand, Anders Mörtberg and Vincent Siles. In the proceedings of CPP 2012.
  25. Towards a Certified Computation of Homology Groups for Digital Images - Jónathan Heras, Maxime Dénès, Gadea Mata, Anders Mörtberg, María Poza and Vincent Siles. In the proceedings of CTIC 2012.
  26. A Formal Proof of the Sasaki-Murao Algorithm - Thierry Coquand, Anders Mörtberg and Vincent Siles. In Journal of Formalized Reasoning, 2012.
  27. A Refinement-Based Approach to Computational Algebra in Coq - Maxime Dénès, Anders Mörtberg and Vincent Siles. In the proceedings of ITP 2012.

PhD thesis

Licentiate thesis

Master thesis