de Mathématiques de Luminy
Unifying static and dynamic denotational semantics.
This work deals with semantics of programming languages (or equivalently, thanks to Curry-Howard isomorphism, with semantics of proofs). We introduce a framework in which both static semantics (Ehrhard's hypercoherences) and dynamic semantics (Hyland-Ong's games), can be presented. The work is carried in a multiplicative sub-system of Laurent's polarized linear logic with weakening. Like Böhm trees for lambda-calculus, designs, adapted from Girard's ludics, play the role of intermediate objets between the syntax and the (two) semantics. Our framework allows us to define a new coherence semantics and to prove its full completeness.