My list of pubblications and preprints is available from a separated page.
Formal Mathematics
Formalization
of Lambda Calculus in Coq and HOL-Light (a characterization
of untyped lambda calculus as initial object of a suitable category of
"Exponential Monads").
