Senior Software Consultant at MLabs consultancy.

Formerly Postdoc in the Programming, Logic and Semantics research group at the Department of Computer Science, IT University of Copenhagen.

I defended my PhD Thesis at the Department of Computer Science and Engineering at Chalmers University of Technology under the supervision of Andreas Abel in September 2018.

- Email: vezzosi.ndr (AT) gmail (DOT) com
- 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

More recent publications are listed at DBLP.

On Induction, Coinduction and Equality in Martin-Löf and Homotopy Type Theory. PhD Thesis, 2018.

Decidability of Conversion for Type Theory in Type Theory (with A. Abel, J. Ohman). PACML, Issue POPL, 2018. doi: 10.1145/3158111.

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.