Andrea Vezzosi

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