Luca Maio

I'm a PhD student in Theoretical Computer Science and Theorem Proving at LMU Munich under the supervision of Jasmin Blanchette.

My main research interests are dependent type theory, interactive as well as automated theorem proving and constructive mathematical logic.

I speak both German and English, feel free to message me with whatever language you prefer.

In German I am open to keep conversations informal, meaning using 'du' instead of 'Sie', depending on your preference. My pronouns are he/him.

You can send me email at <my first name>.<my last name>@ifi.lmu.de or message me on Zulip, make sure to message @Luca Maio (IfI) there.

My office is room L 103, Oettingenstraße 67.

Teaching

Current

Past

  • Bachelor's seminar "Functional Pearls": WiSe 23/24, SoSe 24

  • Master's seminar "Functional Programming and Type Theory": WiSe 23/24, WiSe 24/25

  • Bachelor's practical "Softwareentwicklungspraktikum für Informatik im Nebenfach": WiSe 25/26

  • Teaching Assistant for the lecture "Formale Sprachen und Komplexität" and "Theoretische Informatik für Studierende der Medieninformatik": SoSe 24, SoSe 25, SoSe 26

Research

Drafts

  • From Dependent Type Theory to Dependently Typed Higher Order Logic. Luca Maio, Alexander Bentkamp, Jasmin Blanchette and Sophie Tourret. Draft. Author's PDF

Publications

  • Contextual equivalence in a probabilistic call-by-need lambda-calculus. David Sabel, Manfred Schmidt-Schauß, and Luca Maio. PPDP 2022. 2022. Publisher's page

Theses

  • Bishop’s Compilation Theorem. Luca Maio. Master's Thesis. 2024. Author's PDF

  • The Probabilistic Lambda Calculus with Call-by-Need-Evaluation. Luca Maio. Bachelor's Thesis. 2021. Author's PDF

Mentored Theses

Master's

  • Formalization of Dependently Typed Higher Order Logic in Lean. Orhan Kemal Yüksel. Ongoing.

Bachelor's

  • Implementierung eines Typecheckers und Interpreters für einen λ-Kalkül. Lirona Iseni. Ongoing.

  • Intensional Martin-Löf Type Theory as a Domain Specific Language in Lean. Samuel Leßmann. 2025.

  • Implementing a Higher-Order Unification Algorithm. Petra Murr Yana. 2025.

  • Learning Application for Transforming Context-Sensitive Languages into Linear Bounded Automata. Leon Guz. 2025.

  • Design and Implementation of a Graphical Learning Interface for the Minimization of Deterministic Finite Automata. Tuğba Ünlü. 2024.

  • Implementing an Interactive Learning Tool for Transforming Context-Free Grammars into Normal Forms. Thomas Wölfl. 2024.

  • Implementing a Graphical Learning Interface for the Translation of PDAs into Context-Free Grammars. Daniel Högen. 2024.

  • Implementation of a Graphical Learning Interface for the CYK Algorithm. Sijie Wu. 2024.

  • Implementing a Graphical Learning Interface for the Powerset Construction. Bingzhen Ma. 2024.

To top