Anders Mörtberg

Publication Activity (10 Years)

Years Active: 2012-2024
Publications (10 Years): 29

Top Topics

Programming Language

Theoretic Framework

Top Venues

Math. Struct. Comput. Sci.

Publications

Maximilian Doré, Evan Cavallo, Anders Mörtberg
Automating Boundary Filling in Cubical Agda. CoRR (2024)
Daniel Gratzer, Håkon Gylterud, Anders Mörtberg, Elisabeth Stenholm
The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations. CoRR (2024)
Axel Ljungström, Anders Mörtberg
Computational Synthetic Cohomology Theory in Homotopy Type Theory. CoRR (2024)
Maximilian Doré, Evan Cavallo, Anders Mörtberg
Automating Boundary Filling in Cubical Agda. FSCD (2024)
Thomas Lamiaux, Axel Ljungström, Anders Mörtberg
Computing Cohomology Rings in Cubical Agda. CPP (2023)
Axel Ljungström, Anders Mörtberg
) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda. CoRR (2023)
Axel Ljungström, Anders Mörtberg
) ≅Z/2Z and Computing a Brunerie Number in Cubical Agda. LICS (2023)
Thomas Lamiaux, Axel Ljungström, Anders Mörtberg
Computing Cohomology Rings in Cubical Agda. CoRR (2022)
Guillaume Brunerie, Axel Ljungström, Anders Mörtberg
Synthetic Integral Cohomology in Cubical Agda. CSL (2022)
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
Implementing a category-theoretic framework for typed abstract syntax. CPP (2022)
Max Zeuner, Anders Mörtberg
A Univalent Formalization of Constructive Affine Schemes. TYPES (2022)
Benedikt Ahrens, Simon Huber, Anders Mörtberg
Preface to the MSCS Issue 31.1 (2021) Homotopy Type Theory and Univalent Foundations - Part II. Math. Struct. Comput. Sci. 31 (4) (2021)
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
Implementing a Category-Theoretic Framework for Typed Abstract Syntax. CoRR (2021)
Carlo Angiuli, Evan Cavallo, Anders Mörtberg, Max Zeuner
Internalizing representation independence with univalence. Proc. ACM Program. Lang. 5 (POPL) (2021)
Anders Mörtberg
Cubical methods in homotopy type theory and univalent foundations. Math. Struct. Comput. Sci. 31 (10) (2021)
Andrea Vezzosi, Anders Mörtberg, Andreas Abel
Cubical Agda: A dependently typed programming language with univalence and higher inductive types. J. Funct. Program. 31 (2021)
Benedikt Ahrens, Simon Huber, Anders Mörtberg
Preface to the MSCS Issue 31.1 (2021) Homotopy Type Theory and Univalent Foundations. Math. Struct. Comput. Sci. 31 (1) (2021)
Evan Cavallo, Anders Mörtberg, Andrew W. Swan
Unifying Cubical Models of Univalent Type Theory. CSL (2020)
Anders Mörtberg, Loïc Pujet
Cubical synthetic homotopy theory. CPP (2020)
Carlo Angiuli, Evan Cavallo, Anders Mörtberg, Max Zeuner
Internalizing Representation Independence with Univalence. CoRR (2020)
Andrea Vezzosi, Anders Mörtberg, Andreas Abel
Cubical agda: a dependently typed programming language with univalence and higher inductive types. Proc. ACM Program. Lang. 3 (ICFP) (2019)
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
From Signatures to Monads in UniMath. J. Autom. Reason. 63 (2) (2019)
Thierry Coquand, Simon Huber, Anders Mörtberg
On Higher Inductive Types in Cubical Type Theory. LICS (2018)
Thierry Coquand, Simon Huber, Anders Mörtberg
On Higher Inductive Types in Cubical Type Theory. CoRR (2018)
Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. FLAP 4 (10) (2017)
Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, Vincent Siles
Formalized linear algebra over Elementary Divisor Rings in Coq. Log. Methods Comput. Sci. 12 (2) (2016)
Benedikt Ahrens, Anders Mörtberg
Some Wellfounded Trees in UniMath - Extended Abstract. ICMS (2016)
Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
Cubical Type Theory: a constructive interpretation of the univalence axiom. CoRR (2016)
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
From signatures to monads in UniMath. CoRR (2016)
Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. TYPES (2015)
Cyril Cohen, Anders Mörtberg
A Coq Formalization of Finitely Presented Modules. ITP (2014)
Cyril Cohen, Maxime Dénès, Anders Mörtberg
Refinements for Free! CPP (2013)
Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles
Computing persistent homology within Coq/SSReflect. ACM Trans. Comput. Log. 14 (4) (2013)
Thierry Coquand, Anders Mörtberg, Vincent Siles
Coherent and Strongly Discrete Rings in Type Theory. CPP (2012)
Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles
Computing Persistent Homology within Coq/SSReflect CoRR (2012)
Jónathan Heras, Maxime Dénès, Gadea Mata, Anders Mörtberg, María Poza, Vincent Siles
Towards a Certified Computation of Homology Groups for Digital Images. CTIC (2012)
Maxime Dénès, Anders Mörtberg, Vincent Siles
A Refinement-Based Approach to Computational Algebra in Coq. ITP (2012)
Thierry Coquand, Anders Mörtberg, Vincent Siles
A formal proof of Sasaki-Murao algorithm. J. Formaliz. Reason. 5 (1) (2012)