Anders Mörtberg

Orcid: 0000-0001-9558-6080

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

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

On csauthors.net:

Bibliography

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

Computational Synthetic Cohomology Theory in Homotopy Type Theory.
CoRR, 2024

Automating Boundary Filling in Cubical Agda.
Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction, 2024

2023
Formalizing π<sub>4</sub>(S<sup>^3</sup>) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda.
CoRR, 2023

Formalizing π4(S<sup>3</sup>) ≅Z/2Z and Computing a Brunerie Number in Cubical Agda.
Proceedings of the 38th Annual ACM/IEEE Symposium on Logic in Computer Science, 2023

Computing Cohomology Rings in Cubical Agda.
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

2022
A Univalent Formalization of Constructive Affine Schemes.
Proceedings of the 28th International Conference on Types for Proofs and Programs, 2022

Synthetic Integral Cohomology in Cubical Agda.
Proceedings of the 30th EACSL Annual Conference on Computer Science Logic, 2022

Implementing a category-theoretic framework for typed abstract syntax.
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.
Proc. ACM Program. Lang., 2021

Cubical methods in homotopy type theory and univalent foundations.
Math. Struct. Comput. Sci., 2021

Preface to the MSCS Issue 31.1 (2021) Homotopy Type Theory and Univalent Foundations - Part II.
Math. Struct. Comput. Sci., 2021

Preface to the MSCS Issue 31.1 (2021) Homotopy Type Theory and Univalent Foundations.
Math. Struct. Comput. Sci., 2021

2020
Unifying Cubical Models of Univalent Type Theory.
Proceedings of the 28th EACSL Annual Conference on Computer Science Logic, 2020

Cubical synthetic homotopy theory.
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.
Proc. ACM Program. Lang., 2019

From Signatures to Monads in UniMath.
J. Autom. Reason., 2019

2018
On Higher Inductive Types in Cubical Type Theory.
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.
FLAP, 2017

2016
Formalized linear algebra over Elementary Divisor Rings in Coq.
Log. Methods Comput. Sci., 2016

Some Wellfounded Trees in UniMath - Extended Abstract.
Proceedings of the Mathematical Software - ICMS 2016, 2016

2014
A Coq Formalization of Finitely Presented Modules.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013
Computing persistent homology within Coq/SSReflect.
ACM Trans. Comput. Log., 2013

Refinements for Free!
Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2012
A formal proof of Sasaki-Murao algorithm.
J. Formaliz. Reason., 2012

A Refinement-Based Approach to Computational Algebra in Coq.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Towards a Certified Computation of Homology Groups for Digital Images.
Proceedings of the Computational Topology in Image Context - 4th International Workshop, 2012

Coherent and Strongly Discrete Rings in Type Theory.
Proceedings of the Certified Programs and Proofs - Second International Conference, 2012


  Loading...