Andrea Vezzosi

According to our database, Andrea Vezzosi authored at least 18 papers between 2014 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2023

Formalizing CCS and <i>π</i>-calculus in Guarded Cubical Agda.

Niccolò Veltri, Andrea Vezzosi

J. Log. Algebraic Methods Program., February, 2023

2022

Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks.

Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, Andrea Vezzosi

Proceedings of the LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2, 2022

2021

Two Guarded Recursive Powerdomains for Applicative Simulation.

Rasmus Ejlers Møgelberg, Andrea Vezzosi

Proceedings of the Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, 2021

A model of Clocked Cubical Type Theory.

Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, Andrea Vezzosi

CoRR, 2021

Higher Lenses.

Paolo Capriotti, Nils Anders Danielsson, Andrea Vezzosi

Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021

2020

Partial Univalence in n-truncated Type Theory.

Christian Sattler, Andrea Vezzosi

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

Formalizing π-calculus in guarded cubical Agda.

Niccolò Veltri, Andrea Vezzosi

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

2019

Cubical agda: a dependently typed programming language with univalence and higher inductive types.

Andrea Vezzosi, Anders Mörtberg, Andreas Abel

Proc. ACM Program. Lang., 2019

Guarded Cubical Type Theory.

Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi

J. Autom. Reason., 2019

2018

Decidability of conversion for type theory in type theory.

Andreas Abel, Joakim Öhman, Andrea Vezzosi

Proc. ACM Program. Lang., 2018

2017

Parametric quantifiers for dependent type theory.

Andreas Nuyts, Andrea Vezzosi, Dominique Devriese

Proc. ACM Program. Lang., 2017

Normalization by evaluation for sized dependent types.

Andreas Abel, Andrea Vezzosi, Théo Winterhalter

Proc. ACM Program. Lang., 2017

2016

Executable Relational Specifications of Polymorphic Type Systems Using Prolog.

Ki Yung Ahn, Andrea Vezzosi

Proceedings of the Functional and Logic Programming - 13th International Symposium, 2016

Guarded Cubical Type Theory: Path Equality for Guarded Recursion.

Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi

Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

2015

Lightweight Higher-Order Rewriting in Haskell.

Emil Axelsson, Andrea Vezzosi

Proceedings of the Trends in Functional Programming - 16th International Symposium, 2015

Functions out of Higher Truncations.

Paolo Capriotti, Nicolai Kraus, Andrea Vezzosi

Proceedings of the 24th EACSL Annual Conference on Computer Science Logic, 2015

2014

A Categorical Perspective on Pattern Unification (Extended Abstract).

Andrea Vezzosi, Andreas Abel

Proceedings of the 28th International Workshop on Unification, 2014

A Formalized Proof of Strong Normalization for Guarded Recursive Types.

Andreas Abel, Andrea Vezzosi

Proceedings of the Programming Languages and Systems - 12th Asian Symposium, 2014