A Formalized Proof of Strong Normalization for Guarded Recursive Types. - Andreas Abel 001; Andrea Vezzosi (APLAS, 2014)

A Categorical Perspective on Pattern Unification (Extended Abstract). - Andrea Vezzosi; Andreas Abel 001 (UNIF, 2014)

Functions out of Higher Truncations. - Paolo Capriotti; Nicolai Kraus; Andrea Vezzosi (CSL, 2015)

Lightweight Higher-Order Rewriting in Haskell. - Emil Axelsson; Andrea Vezzosi (TFP, 2015)

Guarded Cubical Type Theory: Path Equality for Guarded Recursion. - Lars Birkedal; Ales Bizjak; Ranald Clouston; Hans Bugge Grathwohl; Bas Spitters; Andrea Vezzosi (CSL, 2016)

Executable Relational Specifications of Polymorphic Type Systems Using Prolog. - Ki Yung Ahn; Andrea Vezzosi (FLOPS, 2016)

Normalization by evaluation for sized dependent types. - Andreas Abel 001; Andrea Vezzosi; Théo Winterhalter (Proc. ACM Program. Lang., 2017)

Parametric quantifiers for dependent type theory. - Andreas Nuyts; Andrea Vezzosi; Dominique Devriese (Proc. ACM Program. Lang., 2017)

Decidability of conversion for type theory in type theory. - Andreas Abel 001; Joakim Öhman; Andrea Vezzosi (Proc. ACM Program. Lang., 2018)

Guarded Cubical Type Theory. - Lars Birkedal; Ales Bizjak; Ranald Clouston; Hans Bugge Grathwohl; Bas Spitters; Andrea Vezzosi (J. Autom. Reason., 2019)

Cubical agda: a dependently typed programming language with univalence and higher inductive types. - Andrea Vezzosi; Anders Mörtberg; Andreas Abel 001 (Proc. ACM Program. Lang., 2019)

Formalizing π-calculus in guarded cubical Agda. - Niccolò Veltri; Andrea Vezzosi (CPP, 2020)

Partial Univalence in n-truncated Type Theory. - Christian Sattler; Andrea Vezzosi (LICS, 2020)

Higher Lenses. - Paolo Capriotti; Nils Anders Danielsson; Andrea Vezzosi (LICS, 2021)

A model of Clocked Cubical Type Theory. - Magnus Baunsgaard Kristensen; Rasmus Ejlers Møgelberg; Andrea Vezzosi (CoRR, 2021)

Two Guarded Recursive Powerdomains for Applicative Simulation. - Rasmus Ejlers Møgelberg; Andrea Vezzosi (MFPS, 2021)

Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks. - Magnus Baunsgaard Kristensen; Rasmus Ejlers Møgelberg; Andrea Vezzosi (LICS, 2022)

Formalizing CCS and π-calculus in Guarded Cubical Agda. - Niccolò Veltri; Andrea Vezzosi (J. Log. Algebraic Methods Program., 2023)