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.

Documents joints

Revenu et logement, Je livre ici quelques éléments de comparaison concernant mon niveau de vie, pour couper court à quelques idées reçues, et un condensé de nombreuses (...)
Revenu et travail d’un enseignant-chercheur, Cet article complète l'article Revenu et logement, en détaillant un peu le budget de mon ménage, mon parcours d'enseignant-chercheur en terme de (...)
Cybersyn (el systemo synco), Au café, mardi 5 avril 2011, j'ai bien vu que, mis à part Antoine Allombert, personne ne connaissait l'histoire de l'extraordinaire projet chilien (...) [jpg, jpg, png]