Andrea Vezzosi

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.

Contact

• Email: vezzosi.ndr (AT) gmail (DOT) com
• Github: http://github.com/Saizan

Software

• 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

Publications and drafts

• 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.