Anders Mörtberg

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