Publications
Papers
- From signatures to monads in UniMath - Benedikt Ahrens, Ralph Matthes and Anders Mörtberg. Preprint 2016. [BibTeX | Code]
- Some Wellfounded Trees in UniMath - Benedikt Ahrens and Anders Mörtberg. In the proceedings of ICMS 2016. [BibTeX]
- 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]
- 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]
- 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 Sasaki-Murao Algorithm - Thierry Coquand, Anders Mörtberg and Vincent Siles. In Journal of Formalized Reasoning 2012. [BibTeX | Code | Slides]
- 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
-
Constructive Algebra in
Type Theory
Defended September 4, 2012. [Slides]