Home | Research | Publications | Teaching | Contacts |
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
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).