Andrea Vezzosi

Publication Activity (10 Years)

Years Active: 2014-2023
Publications (10 Years): 18

Top Topics

Theoretical Basis

Programming Language

Probabilistic Databases

Top Venues

Proc. ACM Program. Lang.

Publications

Niccolò Veltri, Andrea Vezzosi
-calculus in Guarded Cubical Agda. J. Log. Algebraic Methods Program. 131 (2023)
Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, Andrea Vezzosi
Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks. LICS (2022)
Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, Andrea Vezzosi
A model of Clocked Cubical Type Theory. CoRR (2021)
Paolo Capriotti, Nils Anders Danielsson, Andrea Vezzosi
Higher Lenses. LICS (2021)
Rasmus Ejlers Møgelberg, Andrea Vezzosi
Two Guarded Recursive Powerdomains for Applicative Simulation. CoRR (2021)
Andrea Vezzosi, Anders Mörtberg, Andreas Abel
Cubical Agda: A dependently typed programming language with univalence and higher inductive types. J. Funct. Program. 31 (2021)
Niccolò Veltri, Andrea Vezzosi
Formalizing π-calculus in guarded cubical Agda. CPP (2020)
Christian Sattler, Andrea Vezzosi
Partial Univalence in n-truncated Type Theory. CoRR (2020)
Christian Sattler, Andrea Vezzosi
Partial Univalence in n-truncated Type Theory. LICS (2020)
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
Guarded Cubical Type Theory. J. Autom. Reason. 63 (2) (2019)
Andrea Vezzosi, Anders Mörtberg, Andreas Abel
Cubical agda: a dependently typed programming language with univalence and higher inductive types. Proc. ACM Program. Lang. 3 (ICFP) (2019)
Andreas Abel, Joakim Öhman, Andrea Vezzosi
Decidability of conversion for type theory in type theory. Proc. ACM Program. Lang. 2 (POPL) (2018)
Andreas Abel, Andrea Vezzosi, Théo Winterhalter
Normalization by evaluation for sized dependent types. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Andreas Nuyts, Andrea Vezzosi, Dominique Devriese
Parametric quantifiers for dependent type theory. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
Guarded Cubical Type Theory: Path Equality for Guarded Recursion. CSL (2016)
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
Guarded Cubical Type Theory: Path Equality for Guarded Recursion. CoRR (2016)
Ki Yung Ahn, Andrea Vezzosi
Executable Relational Specifications of Polymorphic Type Systems Using Prolog. FLOPS (2016)
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
Guarded Cubical Type Theory. CoRR (2016)
Emil Axelsson, Andrea Vezzosi
Lightweight Higher-Order Rewriting in Haskell. TFP (2015)
Paolo Capriotti, Nicolai Kraus, Andrea Vezzosi
Functions out of Higher Truncations. CoRR (2015)
Paolo Capriotti, Nicolai Kraus, Andrea Vezzosi
Functions out of Higher Truncations. CSL (2015)
Andreas Abel, Andrea Vezzosi
A Formalized Proof of Strong Normalization for Guarded Recursive Types. APLAS (2014)
Andrea Vezzosi, Andreas Abel
A Categorical Perspective on Pattern Unification (Extended Abstract). UNIF (2014)