Coherent and Strongly Discrete Rings in Type Theory. - Thierry Coquand; Anders Mörtberg; Vincent Siles (CPP, 2012)

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; Vincent Siles (CTIC, 2012)

A Refinement-Based Approach to Computational Algebra in Coq. - Maxime Dénès; Anders Mörtberg; Vincent Siles (ITP, 2012)

A formal proof of Sasaki-Murao algorithm. - Thierry Coquand; Anders Mörtberg; Vincent Siles (J. Formaliz. Reason., 2012)

Refinements for Free! - Cyril Cohen; Maxime Dénès; Anders Mörtberg (CPP, 2013)

Computing persistent homology within Coq/SSReflect. - Jónathan Heras; Thierry Coquand; Anders Mörtberg; Vincent Siles (ACM Trans. Comput. Log., 2013)

A Coq Formalization of Finitely Presented Modules. - Cyril Cohen; Anders Mörtberg (ITP, 2014)

Some Wellfounded Trees in UniMath - Extended Abstract. - Benedikt Ahrens; Anders Mörtberg (ICMS, 2016)

Formalized linear algebra over Elementary Divisor Rings in Coq. - Guillaume Cano; Cyril Cohen; Maxime Dénès; Anders Mörtberg; Vincent Siles (Log. Methods Comput. Sci., 2016)

Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. - Cyril Cohen; Thierry Coquand; Simon Huber; Anders Mörtberg (FLAP, 2017)

On Higher Inductive Types in Cubical Type Theory. - Thierry Coquand; Simon Huber; Anders Mörtberg (LICS, 2018)

From Signatures to Monads in UniMath. - Benedikt Ahrens; Ralph Matthes; Anders Mörtberg (J. Autom. Reason., 2019)

Cubical agda: a dependently typed programming language with univalence and higher inductive types. - Andrea Vezzosi; Anders Mörtberg; Andreas Abel 001 (Proc. ACM Program. Lang., 2019)

Cubical synthetic homotopy theory. - Anders Mörtberg; Loïc Pujet (CPP, 2020)

Unifying Cubical Models of Univalent Type Theory. - Evan Cavallo; Anders Mörtberg; Andrew W. Swan (CSL, 2020)

Preface to the MSCS Issue 31.1 (2021) Homotopy Type Theory and Univalent Foundations. - Benedikt Ahrens; Simon Huber; Anders Mörtberg (Math. Struct. Comput. Sci., 2021)

Preface to the MSCS Issue 31.1 (2021) Homotopy Type Theory and Univalent Foundations - Part II. - Benedikt Ahrens; Simon Huber; Anders Mörtberg (Math. Struct. Comput. Sci., 2021)

Cubical methods in homotopy type theory and univalent foundations. - Anders Mörtberg (Math. Struct. Comput. Sci., 2021)

Internalizing representation independence with univalence. - Carlo Angiuli; Evan Cavallo; Anders Mörtberg; Max Zeuner (Proc. ACM Program. Lang., 2021)

Implementing a category-theoretic framework for typed abstract syntax. - Benedikt Ahrens; Ralph Matthes; Anders Mörtberg (CPP, 2022)

Synthetic Integral Cohomology in Cubical Agda. - Guillaume Brunerie; Axel Ljungström; Anders Mörtberg (CSL, 2022)

A Univalent Formalization of Constructive Affine Schemes. - Max Zeuner; Anders Mörtberg (TYPES, 2022)

Computing Cohomology Rings in Cubical Agda. - Thomas Lamiaux; Axel Ljungström; Anders Mörtberg (CPP, 2023)

Formalizing π4(S3) ≅Z/2Z and Computing a Brunerie Number in Cubical Agda. - Axel Ljungström; Anders Mörtberg (LICS, 2023)

Formalizing π4(S^3) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda. - Axel Ljungström; Anders Mörtberg (CoRR, 2023)

Automating Boundary Filling in Cubical Agda. - Maximilian Doré; Evan Cavallo; Anders Mörtberg (FSCD, 2024)

Computational Synthetic Cohomology Theory in Homotopy Type Theory. - Axel Ljungström; Anders Mörtberg (CoRR, 2024)

The category of iterative sets in homotopy type theory and univalent foundations. - Daniel Gratzer; Håkon Robbestad Gylterud; Anders Mörtberg; Elisabeth Stenholm (Math. Struct. Comput. Sci., 2024)