Publications
Papers
 Cubical Synthetic Homotopy Theory  Anders Mörtberg, Loïc Pujet. Preprint 2019. Accepted at Certified Programs and Proofs, CPP 2020. [BibTeX]
 Unifying Cubical Models of Univalent Type Theory  Evan Cavallo, Anders Mörtberg, Andrew W Swan. Preprint 2019. Accepted at Computer Science Logic, CSL 2020. [BibTeX]
 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. Winner of Distinguished Paper Award. [BibTeX  Code]
 On Higher Inductive Types in Cubical Type Theory  Thierry Coquand, Simon Huber and Anders Mörtberg. In the proceedings of LICS 2018. [BibTeX  Code]
 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). [BibTeX  Code]
 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. [BibTeX  Code]
 Some Wellfounded Trees in UniMath  Benedikt Ahrens and Anders Mörtberg. In the proceedings of ICMS 2016. [BibTeX]
 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. [BibTeX  Code]
 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. [BibTeX  Code]
 A Coq Formalization of Finitely Presented Modules  Cyril Cohen and Anders Mörtberg. In the proceedings of ITP 2014. [BibTeX  Code  Slides]
 Computing Persistent Homology within Coq/SSReflect  Jónathan Heras, Thierry Coquand, Anders Mörtberg and Vincent Siles. In ACM Transactions on Computational Logic 2013. [BibTeX  Code]
 Refinements for free!  Cyril Cohen, Maxime Dénès and Anders Mörtberg. In the proceedings of CPP 2013. [BibTeX  Code]
 Coherent and Strongly Discrete Rings in Type Theory  Thierry Coquand, Anders Mörtberg and Vincent Siles. In the proceedings of CPP 2012. [BibTeX  Code  Slides]
 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. [BibTeX  Code]
 A Formal Proof of the SasakiMurao Algorithm  Thierry Coquand, Anders Mörtberg and Vincent Siles. In Journal of Formalized Reasoning 2012. [BibTeX  Code  Slides]
 A RefinementBased Approach to Computational Algebra in Coq  Maxime Dénès, Anders Mörtberg and Vincent Siles. In the proceedings of ITP 2012. [BibTeX  Code]
PhD thesis
Licentiate thesis

Constructive Algebra in
Type Theory
Defended September 4, 2012. [Slides]