Andrea Vezzosi
Title
Cited by
Cited by
Year
Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types
A Vezzosi, A Mörtberg, A Abel
63*
Guarded cubical type theory
L Birkedal, A Bizjak, R Clouston, HB Grathwohl, B Spitters, A Vezzosi
Journal of Automated Reasoning, 1-43, 2018
52*2018
Parametric quantifiers for dependent type theory
A Nuyts, A Vezzosi, D Devriese
Proceedings of the ACM on Programming Languages 1 (ICFP), 32, 2017
432017
Decidability of conversion for type theory in type theory
A Abel, J Öhman, A Vezzosi
Proceedings of the ACM on Programming Languages 2 (POPL), 23, 2017
362017
Normalization by evaluation for sized dependent types
A Abel, A Vezzosi, T Winterhalter
Proceedings of the ACM on Programming Languages 1 (ICFP), 33, 2017
28*2017
A formalized proof of strong normalization for guarded recursive types
A Abel, A Vezzosi
Asian Symposium on Programming Languages and Systems, 140-158, 2014
202014
Formalizing 𝜋-calculus in guarded cubical Agda
N Veltri, A Vezzosi
Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020
82020
Executable relational specifications of polymorphic type systems using prolog
KY Ahn, A Vezzosi
International Symposium on Functional and Logic Programming, 109-125, 2016
62016
Functions out of higher truncations
P Capriotti, N Kraus, A Vezzosi
arXiv preprint arXiv:1507.01150, 2015
62015
Heterogeneous equality incompatible with univalence even–without-K, 2015
A Vezzosi
URL https://github. com/agda/agda, 0
5
Tog, a prototypical implementation of dependent types
F Mazzoli, NA Danielsson, U Norell, A Vezzosi, A Abel
GitHub Repository https://github. com/bitonic/tog, 2017
42017
Higher lenses
P Capriotti, NA Danielsson, A Vezzosi
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-13, 2021
32021
Lightweight Higher-Order Rewriting in Haskell
E Axelsson, A Vezzosi
International Symposium on Trends in Functional Programming, 1-21, 2015
22015
Guarded recursive types in type theory
A Vezzosi
Chalmers University of Technology, 2015
22015
A model of Clocked Cubical Type Theory
MB Kristensen, RE Møgelberg, A Vezzosi
arXiv preprint arXiv:2102.01969, 2021
12021
Streams for cubical type theory
A Vezzosi
12017
A model of Clocked Cubical Type Theory
M Baunsgaard Kristensen, R Ejlers Møgelberg, A Vezzosi
arXiv e-prints, arXiv: 2102.01969, 2021
2021
Partial Univalence in n-truncated Type Theory
C Sattler, A Vezzosi
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer …, 2020
2020
On Induction, Coinduction and Equality in Martin-Löf and Homotopy Type Theory
A Vezzosi
PQDT-Global, 2018
2018
Adding Cubes to Agda
A Vezzosi
2017
The system can't perform the operation now. Try again later.
Articles 1–20