| 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 | 410 | 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 | 146 | 2021 |
| Refinements for free! C Cohen, M Dénès, A Mörtberg International Conference on Certified Programs and Proofs, 147-162, 2013 | 103 | 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 | 94 | 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 | 71 | 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 | 34 | 2021 |
| 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 | 27 | 2013 |
| 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 | 26 | 2012 |
| Unifying cubical models of univalent type theory E Cavallo, A Mörtberg, AW Swan 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), 2020 | 25 | 2020 |
| 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 | 22 | 2016 |
| Synthetic integral cohomology in cubical agda G Brunerie, A Ljungström, A Mörtberg 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), 2022 | 17* | 2022 |
| Cubical synthetic homotopy theory A Mörtberg, L Pujet Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 13 | 2020 |
| From signatures to monads in unimath B Ahrens, R Matthes, A Mörtberg Journal of Automated Reasoning 63 (2), 285-318, 2019 | 13 | 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 | 12 | 2022 |
| A formal proof of Sasaki-Murao algorithm T Coquand, A Mörtberg, V Siles Journal of Formalized Reasoning 5 (1), 27-36, 2012 | 10 | 2012 |
| 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 |
| 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 | 5 | 2023 |
| Formalizing and Computing a Brunerie Number in Cubical Agda A Ljungström, A Mörtberg Logic in Computer Science (LICS), 2023 | 4* | 2023 |
