Anders Mörtberg

According to our database, Anders Mörtberg authored at least 28 papers between 2012 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations.

Daniel Gratzer, Håkon Robbestad Gylterud, Anders Mörtberg, Elisabeth Stenholm

CoRR, 2024

Computational Synthetic Cohomology Theory in Homotopy Type Theory.

Axel Ljungström, Anders Mörtberg

CoRR, 2024

Automating Boundary Filling in Cubical Agda.

Maximilian Doré, Evan Cavallo, Anders Mörtberg

Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction, 2024

2023

Formalizing π₄(S^{^3}) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda.

Axel Ljungström, Anders Mörtberg

CoRR, 2023

Formalizing π4(S³) ≅Z/2Z and Computing a Brunerie Number in Cubical Agda.

Axel Ljungström, Anders Mörtberg

Proceedings of the 38th Annual ACM/IEEE Symposium on Logic in Computer Science, 2023

Computing Cohomology Rings in Cubical Agda.

Thomas Lamiaux, Axel Ljungström, Anders Mörtberg

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

2022

A Univalent Formalization of Constructive Affine Schemes.

Max Zeuner, Anders Mörtberg

Proceedings of the 28th International Conference on Types for Proofs and Programs, 2022

Synthetic Integral Cohomology in Cubical Agda.

Guillaume Brunerie, Axel Ljungström, Anders Mörtberg

Proceedings of the 30th EACSL Annual Conference on Computer Science Logic, 2022

Implementing a category-theoretic framework for typed abstract syntax.

Benedikt Ahrens, Ralph Matthes, Anders Mörtberg

Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

2021

Internalizing representation independence with univalence.

Carlo Angiuli, Evan Cavallo, Anders Mörtberg, Max Zeuner

Proc. ACM Program. Lang., 2021

Cubical methods in homotopy type theory and univalent foundations.

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

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

2020

Unifying Cubical Models of Univalent Type Theory.

Evan Cavallo, Anders Mörtberg, Andrew W. Swan

Proceedings of the 28th EACSL Annual Conference on Computer Science Logic, 2020

Cubical synthetic homotopy theory.

Anders Mörtberg, Loïc Pujet

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

2019

Cubical agda: a dependently typed programming language with univalence and higher inductive types.

Andrea Vezzosi, Anders Mörtberg, Andreas Abel

Proc. ACM Program. Lang., 2019

From Signatures to Monads in UniMath.

Benedikt Ahrens, Ralph Matthes, Anders Mörtberg

J. Autom. Reason., 2019

2018

On Higher Inductive Types in Cubical Type Theory.

Thierry Coquand, Simon Huber, Anders Mörtberg

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

2017

Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom.

Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg

FLAP, 2017

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

Some Wellfounded Trees in UniMath - Extended Abstract.

Benedikt Ahrens, Anders Mörtberg

Proceedings of the Mathematical Software - ICMS 2016, 2016

2014

A Coq Formalization of Finitely Presented Modules.

Cyril Cohen, Anders Mörtberg

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013

Computing persistent homology within Coq/SSReflect.

Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles

ACM Trans. Comput. Log., 2013

Refinements for Free!

Cyril Cohen, Maxime Dénès, Anders Mörtberg

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2012

A formal proof of Sasaki-Murao algorithm.

Thierry Coquand, Anders Mörtberg, Vincent Siles

J. Formaliz. Reason., 2012

A Refinement-Based Approach to Computational Algebra in Coq.

Maxime Dénès, Anders Mörtberg, Vincent Siles

Proceedings of the Interactive Theorem Proving - Third International Conference, 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

Proceedings of the Computational Topology in Image Context - 4th International Workshop, 2012

Coherent and Strongly Discrete Rings in Type Theory.

Thierry Coquand, Anders Mörtberg, Vincent Siles

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012