Alessio Ferrarini

I am a third-year Computer Science Ph.D. student at IMDEA Software. Feel free to contact me at alessio.ferrarini@imdea.org.

Research

My research focuses on programming language theory, type theory, refinement types, semantics, and formal verification. I contribute to the development of Liquid Haskell. I am very fortunate to be advised by Niki Vazou.

Publications

• "PLEX: Normalization for Refinement Types" - Alessio Ferrarini, Niki Vazou, Wouter Swierstra - OOPSLA 2026
  • Official version (ACM Digital Library)
  • Preprint (PDF)
  • Artifact (Zenodo)
• "Large Elimination and Indexed Types in Refinement Types" - Alessio Ferrarini, Niki Vazou - TYPES 2025
  • Extended abstract (PDF)
  • Slides (PDF)

Supervision

• Co-supervised the MSc thesis "Towards Formalisation of Gödel’s First Incompleteness Theorem in Liquid Haskell" - Alejandro Soriano Compta - Universidad Politécnica de Madrid, 2026

Tutorials

• "Solid code with Liquid Types!" by Alessio Ferrarini, Pablo Castellanos - Lambda World 2025, Cádiz, Spain
  • Notes for the first part (PDF)
  • Material (GitHub)

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.

Theses

• "Abstract Hoare Logic" - MSc Thesis, University of Padua, 2024
  • Deposited version
• "Implementation of a Static Typechecker and Optimizations for a Programming Language" - BSc Thesis, University of Padua, 2022
  • Deposited version