Institut de Mathématiques de Luminy

Abstracts : publications 2000


Bucciarelli Antonio and Ehrhard Thomas

We study the notion of logical relation in the coherence space semantics of multiplicative-additive linear logic . We show that, when the ground-type logical relation is "closed under restrictions", the logical relation associated to any type can be seen as a map associating facts of a phase space to families of points of the web of the corresponding coherence space. We introduce a sequent calculus extension of whose formulae denote these families of points. This logic (where I is a set of indexes) admits a truth-value semantics in the previously mentioned phase space, and this truth-value semantics faithfully describes the logical relation model we started from. Then we generalize this notion of phase space, we prove a truth-value completeness result for and we derive from any phase model of a denotational model for . Using the truth-value completeness result, we obtain a weak denotational completeness result based on this new denotational semantics.

Author Keywords: Denotational semantics; Logical relations; Linear logic; Sequent calculus; Phase semantics



Last update : october 24, 2000, EL.