Seguir
Andrea Vezzosi
Andrea Vezzosi
Postdoc, IT University Copenhagen
Dirección de correo verificada de itu.dk - Página principal
Título
Citado por
Citado por
Año
Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types
A Vezzosi, A Mörtberg, A Abel
146*
Guarded cubical type theory
L Birkedal, A Bizjak, R Clouston, HB Grathwohl, B Spitters, A Vezzosi
Journal of Automated Reasoning, 1-43, 2018
71*2018
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
702017
Parametric quantifiers for dependent type theory
A Nuyts, A Vezzosi, D Devriese
Proceedings of the ACM on Programming Languages 1 (ICFP), 32, 2017
552017
Normalization by evaluation for sized dependent types
A Abel, A Vezzosi, T Winterhalter
Proceedings of the ACM on Programming Languages 1 (ICFP), 33, 2017
36*2017
Formalizing 𝜋-calculus in guarded cubical Agda
N Veltri, A Vezzosi
Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020
262020
A formalized proof of strong normalization for guarded recursive types
A Abel, A Vezzosi
Asian Symposium on Programming Languages and Systems, 140-158, 2014
232014
Greatest hits: Higher inductive types in coinductive definitions via induction under clocks
M Baunsgaard Kristensen, RE Mogelberg, A Vezzosi
Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer …, 2022
142022
Functions out of higher truncations
P Capriotti, N Kraus, A Vezzosi
arXiv preprint arXiv:1507.01150, 2015
92015
Two guarded recursive powerdomains for applicative simulation
RE Møgelberg, A Vezzosi
arXiv preprint arXiv:2112.14056, 2021
82021
Executable relational specifications of polymorphic type systems using prolog
KY Ahn, A Vezzosi
Functional and Logic Programming: 13th International Symposium, FLOPS 2016 …, 2016
72016
Heterogeneous equality incompatible with univalence even–without-K, 2015
A Vezzosi
URL https://github. com/agda/agda, 0
5
Higher lenses
P Capriotti, NA Danielsson, A Vezzosi
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-13, 2021
42021
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
Decidability of conversion for type theory in type theory. PACMPL 2 (POPL), 23: 1–23: 29 (2018)
A Abel, J Öhman, A Vezzosi
4
Formalizing CCS and π-calculus in Guarded Cubical Agda
N Veltri, A Vezzosi
Journal of Logical and Algebraic Methods in Programming 131, 100846, 2023
22023
A model of clocked cubical type theory
MB Kristensen, RE Møgelberg, A Vezzosi
arXiv preprint arXiv:2102.01969, 2021
22021
Streams for cubical type theory
A Vezzosi
22017
Lightweight Higher-Order Rewriting in Haskell
E Axelsson, A Vezzosi
Trends in Functional Programming: 16th International Symposium, TFP 2015 …, 2016
22016
Total (Co) Programming with Guarded Recursion
A Vezzosi
21st International Conference on Types for Proofs and Programs (TYPES 2015 …, 2015
22015
El sistema no puede realizar la operación en estos momentos. Inténtalo de nuevo más tarde.
Artículos 1–20