Andrea Vezzosi in nLab
Selected writings
Selected writings
Introducing the programming language Cubical Agda implementing univalent cubical homotopy type theory with higher inductive types:
- Andrea Vezzosi, Anders Mörtberg, Andreas Abel, Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types, Proceedings of the ACM on Programming Languages 3 ICFP 87 (2019) 1–29 [doi:10.1145/3341691, pdf]
On cubical homotopy type theory implemented in the proof assistant Cubical Agda:
-
Guarded Cubical Type Theory: Path Equality for Guarded Recursion, Lars Birkedal, Aleš Bizjak?, Ranald Clouston?, Hans Bugge Grathwohl?, Bas Spitters, Andrea Vezzosi, (arXiv:1606.05223)
-
Magnus Baunsgaard Kristensen?, Rasmus Ejlers Møgelberg, Andrea Vezzosi, Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks (arXiv:2102.01969)
Last revised on February 13, 2025 at 18:44:32. See the history of this page for a list of all contributions to it.