Domenico Ruoppolo
Mobility Reading Group, Department of Computing, Faculty of Engineering, Imperial College London, UK

tableau"

Home                   Research                   Publications                   Teaching                   Contacts                  

Research

I am interested in logical proofs and (abstract) programs along the line of the Curry-Howard correspondence.
My perspective on the subject is mostly influenced by denotational semantics and linear logic.
I enjoy handling abstract categorical axiomatizations as well as more concrete mathematical models of very
idealized programming languages, such as λ-calculi and π-calculi.

A handful of keywords which I like to think that concern me:
λ-calculi (in particular their denotational semantics)
π-calculi (in particular their typing discipline) type theory (in particular intersection and linear type systems)
proof theory (classical, intuitionistic, linear logic)
categorical semantics of programming

Currently, I am focusing on type systems for concurrency.

Here is a poster from 2018 presenting all my other research interests.
(Yes, it is in French...but it is colorful! So it may be worth a quick look...)

During my PhD (2012-2016), my focus was on resource-sensitive denotational models of the old good
untyped λ-calculus. A brief introduction to this kind of stuff can be found in this old research statement
of mine (update: sping 2017).