Unifying static and dynamic denotational semantics
pré-publication IML 2004
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.