Denotational Completeness Revisited
Thomas Streicher · Electronic Notes in Theoretical Computer Science · 1999
We define a notion of Kripke logical predicate for models of classical linear logic. A Kripke logical predicate on a type A will be a set of generalised elements of A satisfying certain closure properties. Denotations of proofs of A will be characterised as those global elements of A satisfying all Kripke logical predicates on A. The work reported in this paper was done during my visit of the research group Logique de la Programmation at the CNRS in Luminy (Marseille) in autumn 1998. In particular I am indebted Thomas Ehrhard who patiently explained to me his work on non–Kripke logical relations on the coherence space model of Linear Logic.