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
412 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
95 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
35 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