Contact information
I work at PPS under the supervision of Thomas Ehrhard and Pierre-Louis Curien.
- Mind the change of domain name.
Research activities
I study the correspondence between proofs and programmes, at the interface between proof theory in mathematical logic, and the semantics of programming languages in theoretical computer science.
My path led me to study the contributions of linear logic, and in particular of Girard's analysis of the notion of polarity, to this correspondence. Polarisation contributes to the understanding of:
- the computational contents of proofs through the classical realisability of Krivine,
- double-negation translations,
- the semantics of higher-order programming languages.
The hypothesis of polarisation
Intuitionism already made the practical distinction between negative connectives (∀,⇒...) and positive connectives (∨,∃...). Polarisation gives a status to these polarities by claiming they live in different worlds from the point of view of computation. Understanding how the two worlds communicate then allows us to throw light on various phenomena related to polarities.
Classical realisability
The paper “Focalisation and classical realisability” illustrates the above point of view by extending Krivine's classical realisability to Girard's polarised classical logic LC: in addition to negatives that live in the polar of a set of stacks, positives live in the bipolar of a set of values. The explicit polarities of LC simplify the theory on various aspects, thanks to a sharper control on constructivity properties.
CPS translations
Polarisation also has a role in the understanding of continuation-passing style (CPS) translations: polarities can be used to distinguish continuations on whether they are meant to be passed or meant to be applied. This way polarities distinguish in the source language expressions that are strict from ones that are lazy.
Based on this interpretation, I describe in “From delimited CPS to polarisation” how polarities (and linear logic) help understand various CPS translations for calculi with delimited control operators that appeared in the literature.
System L
One of the main technical aspects of my work is the use of a practical term syntax for polarised classical logic which is inspired by Curien and Herbelin's “mu mu-tilde” calculus (or system “L”). We believe that system L is a canonical notation for sequent calculus. (See e.g. “The duality of computation under focus”.)
In addition, my design goal with the “focalising” variant was to have a tool for the thought that expresses the more properties of the semantics in the fewest possible symbols and equations. This is possible because system L emphasizes the interactive aspects of computation over the usual functional aspects of languages.
My current goal is to further show how contributions from denotational semantics and functional programming help investigate the proofs-as-programs correspondence.