nLab Andrea Vezzosi

Homepage

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)

category: people