Alessio Ferrarini – Ph.D. Student in Programming Languages and Type Theory

I'm a first-year Computer Science Ph.D. student at IMDEA Software.

Feel free to contact me at alessio.ferrarini@imdea.org.

Research

My research interests lie in programming languages and verification, with a focus on type theory, functional programming, logic, and semantics.

My work right now focuses on the theoretical aspects of refinement types, and I contribute to the development of Liquid Haskell.

I'm very fortunate to be advised by Niki Vazou.

Publications

"Something under submission" by Alessio Ferrarini, Niki Vazou, Wouter Swierstra

Talks and Workshops

"Solid code with Liquid Types!" by Alessio Ferrarini, Pablo Castellanos - Lambda World 2025, Cádiz, Spain [Notes (only first part) (PDF), Material (GitHub)]
"Large Elimination and Indexed Types in Refinement Types" by Alessio Ferrarini, Niki Vazou - TYPES 2025, Glasgow, UK [Extended abstract (PDF), Slides (PDF)]

Education

I obtained my Master's and Bachelor's degrees in Computer Science from the University of Padua in Italy. During my studies, I had the opportunity to study abroad at VU Amsterdam in the Netherlands.

MSc thesis

For my Master's thesis, I developed a generalization of Hoare logic called Abstract Hoare logic, a "semantics first" approach to obtain sound and complete partial correctness/incorrectness program logics.

BSc thesis

For my Bachelor's thesis, I developed a type system and implemented some optimizations for the CPL programming language used in one of the biggest Italian software development firms.