Publications

Papers

  1. From signatures to monads in UniMath - Benedikt Ahrens, Ralph Matthes and Anders Mörtberg. Preprint 2016. [BibTeX | Code]
  2. Some Wellfounded Trees in UniMath - Benedikt Ahrens and Anders Mörtberg. In the proceedings of ICMS 2016. [BibTeX]
  3. 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 2016. [BibTeX | Code]
  4. 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]
  5. A Coq Formalization of Finitely Presented Modules - Cyril Cohen and Anders Mörtberg. In the proceedings of ITP 2014. [BibTeX | Code | Slides]
  6. 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]
  7. Refinements for free! - Cyril Cohen, Maxime Dénès and Anders Mörtberg. In the proceedings of CPP 2013. [BibTeX | Code]
  8. 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]
  9. 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]
  10. A Formal Proof of the Sasaki-Murao Algorithm - Thierry Coquand, Anders Mörtberg and Vincent Siles. In Journal of Formalized Reasoning 2012. [BibTeX | Code | Slides]
  11. 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. [BibTeX | Code]

PhD thesis

Licentiate thesis

Master thesis