PhD Student, Computing Science division, Department of Computer Science and Engineering, Chalmers University of Technology.

- Email: vezzosi (AT) chalmers (DOT) se
- Github: http://github.com/Saizan

- Library and examples for agda --cubical
- Examples for agda/parametric
- Agda with a flat modality (based on spatial type theory)
- Guarded Cubical Type Theory prototype
- Agda formalization of Pattern Unification for STLC

Decidability of Conversion for Type Theory in Type Theory (with A. Abel, J. Ohman). To appear in PACML, Issue POPL, 2018.

Normalization by evaluation for sized dependent types (with A. Abel, T. Winterhalter). PACMPL, Issue ICFP, 2017. doi: 10.1145/3110277.

Parametric quantifiers for dependent type theory (with A. Nuyts, D. Devriese). PACMPL, Issue ICFP, 2017. doi: 10.1145/3110276.

Streams for Cubical Type Theory [pdf]. Unpublished note, 2017.

Executable relational specifications of polymorphic type systems using prolog (with K. Ahn). LNCS: FLOPS 2016; Kochi; Japan, 2016. doi: 10.1007/978-3-319-29604-3_8.

Guarded Cubical Type Theory: Path Equality for Guarded Recursion [arxiv] (with L. Birkedal, A. Bizjak, R. Clouston, H. Grathwohl, B. Spitters). 25th EACSL Annual Conference on Computer Science Logic. CSL, 2016. doi: 10.4230/LIPIcs.CSL.2016.23.

Lightweight Higher-Order Rewriting in Haskell (with E. Axelsson). Trends in Functional Programming, 2015. doi: 10.1007/978-3-319-39110-6_1. Received the "John McCarthy Best Article" and the "David Turner Best Student Article" awards.

Functions out of Higher Truncations [arxiv] (with P. Capriotti, N. Kraus). 24th EACSL Annual Conference on Computer Science Logic. CSL, 2015. doi: 10.4230/LIPIcs.CSL.2015.359.

Guarded Recursive Types in Type Theory [pdf]. Licenciate Thesis, Chalmers University of Technology, 2015.

A formalized proof of strong normalization for guarded recursive types (with A. Abel). LNCS: APLAS 2014; Singapore, 2014. doi: 10.1007/978-3-319-12736-1_8.

A categorical perspective on pattern unification [pdf] (with A. Abel). UNIF Workshop, 2014.