Publications

Papers

  1. On Higher Inductive Types in Cubical Type Theory - Thierry Coquand, Simon Huber and Anders Mörtberg. In the proceedings of LICS 2018. [BibTeX | Code]
  2. 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]
  3. From signatures to monads in UniMath - Benedikt Ahrens, Ralph Matthes and Anders Mörtberg. In Journal of Automated Reasoning 2017. To appear in Special Issue on Homotopy Type Theory and Univalent Foundations. [BibTeX | Code]
  4. Some Wellfounded Trees in UniMath - Benedikt Ahrens and Anders Mörtberg. In the proceedings of ICMS 2016. [BibTeX]
  5. 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. To appear 2018. [BibTeX | Code]
  6. 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]
  7. A Coq Formalization of Finitely Presented Modules - Cyril Cohen and Anders Mörtberg. In the proceedings of ITP 2014. [BibTeX | Code | Slides]
  8. 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]
  9. Refinements for free! - Cyril Cohen, Maxime Dénès and Anders Mörtberg. In the proceedings of CPP 2013. [BibTeX | Code]
  10. 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]
  11. 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]
  12. 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]
  13. 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