| 2026 | LICS | A Computer Formalisation of the Serre Finiteness Theorem. | Reid Barton, Axel Ljungstrm, Owen Milner, Anders Mrtberg |
| 2024 | FSCD | Automating Boundary Filling in Cubical Agda. | Maximilian Dor, Evan Cavallo, Anders Mrtberg |
| 2023 | CPP | Computing Cohomology Rings in Cubical Agda. | Thomas Lamiaux, Axel Ljungstrm, Anders Mrtberg |
| 2023 | LICS | Formalizing π4(S | Axel Ljungstrm, Anders Mrtberg |
| 2022 | CPP | Implementing a category-theoretic framework for typed abstract syntax. | Benedikt Ahrens, Ralph Matthes, Anders Mrtberg |
| 2022 | CSL | Synthetic Integral Cohomology in Cubical Agda. | Guillaume Brunerie, Axel Ljungstrm, Anders Mrtberg |
| 2020 | CPP | Cubical synthetic homotopy theory. | Anders Mrtberg, Loc Pujet |
| 2020 | CSL | Unifying Cubical Models of Univalent Type Theory. | Evan Cavallo, Anders Mrtberg, Andrew W. Swan |
| 2018 | LICS | On Higher Inductive Types in Cubical Type Theory. | Thierry Coquand, Simon Huber, Anders Mrtberg |
| 2014 | ITP | A Coq Formalization of Finitely Presented Modules. | Cyril Cohen, Anders Mrtberg |
| 2013 | CPP | Refinements for Free! | Cyril Cohen, Maxime Dns, Anders Mrtberg |
| 2012 | CPP | Coherent and Strongly Discrete Rings in Type Theory. | Thierry Coquand, Anders Mrtberg, Vincent Siles |
| 2012 | ITP | A Refinement-Based Approach to Computational Algebra in Coq. | Maxime Dns, Anders Mrtberg, Vincent Siles |