| Cubical type theory: a constructive interpretation of the univalence axiom C Cohen, T Coquand, S Huber, A Mörtberg arXiv preprint arXiv:1611.02108, 2016 | 448 | 2016 |
| Cubical Agda: A dependently typed programming language with univalence and higher inductive types A Vezzosi, A Mörtberg, A Abel Journal of Functional Programming 31, e8, 2021 | 176 | 2021 |
| Refinements for free! C Cohen, M Dénès, A Mörtberg International Conference on Certified Programs and Proofs, 147-162, 2013 | 110 | 2013 |
| On higher inductive types in cubical type theory T Coquand, S Huber, A Mörtberg Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer …, 2018 | 107 | 2018 |
| A Refinement-Based Approach to Computational Algebra in Coq M Dénès, A Mörtberg, V Siles International Conference on Interactive Theorem Proving, 83-98, 2012 | 75 | 2012 |
| Internalizing representation independence with univalence C Angiuli, E Cavallo, A Mörtberg, M Zeuner Proceedings of the ACM on Programming Languages 5 (POPL), 1-30, 2021 | 43 | 2021 |
| Unifying cubical models of univalent type theory E Cavallo, A Mörtberg, AW Swan 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), 14: 1-14: 17, 2020 | 31 | 2020 |
| Computing persistent homology within Coq/SSReflect J Heras, T Coquand, A Mörtberg, V Siles ACM Transactions on Computational Logic (TOCL) 14 (4), 1-16, 2013 | 26 | 2013 |
| Synthetic integral cohomology in cubical agda G Brunerie, A Ljungström, A Mörtberg 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), 11: 1-11: 19, 2022 | 25* | 2022 |
| Towards a certified computation of homology groups for digital images J Heras, M Dénès, G Mata, A Mörtberg, M Poza, V Siles Computational Topology in Image Context: 4th International Workshop, CTIC …, 2012 | 23 | 2012 |
| Formalized linear algebra over elementary divisor rings in Coq G Cano, C Cohen, M Dénès, A Mörtberg, V Siles Logical Methods in Computer Science 12, 2016 | 21 | 2016 |
| Cubical synthetic homotopy theory A Mörtberg, L Pujet Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 20 | 2020 |
| From signatures to monads in UniMath B Ahrens, R Matthes, A Mörtberg Journal of Automated Reasoning 63 (2), 285-318, 2019 | 14 | 2019 |
| Implementing a category-theoretic framework for typed abstract syntax B Ahrens, R Matthes, A Mörtberg Proceedings of the 11th ACM SIGPLAN International Conference on Certified …, 2022 | 13 | 2022 |
| A formal proof of Sasaki-Murao algorithm T Coquand, A Mörtberg, V Siles Journal of Formalized Reasoning 5 (1), 27-36, 2012 | 11 | 2012 |
| Formalizing and Computing a Brunerie Number in Cubical Agda A Ljungström, A Mörtberg Logic in Computer Science (LICS), 2023 | 10* | 2023 |
| Computing cohomology rings in cubical agda T Lamiaux, A Ljungström, A Mörtberg Proceedings of the 12th ACM SIGPLAN International Conference on Certified …, 2023 | 9 | 2023 |
| Constructive algebra in functional programming and type theory A Mörtberg Mathematics, Algorithms and Proofs 2010, 2010 | 8 | 2010 |
| Coherent and strongly discrete rings in type theory T Coquand, A Mörtberg, V Siles Certified Programs and Proofs: Second International Conference, CPP 2012 …, 2012 | 7 | 2012 |
| A formalization of the initiality conjecture in Agda G Brunerie, M de Boer, PL Lumsdaine, A Mörtberg Slides from a talk about joint work with Menno de Boer, Peter Lumsdaine, and …, 2019 | 6* | 2019 |
