Coherent semantics

Revision as of 17:05, 7 February 2009

Coherent semantics was invented by Girard in the paper The system F, 15 years later. It is a refinement of the former qualitative domains that allows for building an interpretation of system F terms, that is for second order quantifiers.

Coherent semantics is based on the notion of stable functions that was initially proposed by Gérard Berry. Stability is a condition on Scott continuous functions that expresses the determinism of the relation between the output and the input: the typical Scott continuous but non stable function is the parallel or because when the two inputs are both set to true, only one of them is the reason why the result is true but there is no way to determine which one.

Although coherent semantics allowed to solve for the first time the old standing problem of building a denotationnal semantics for polymorphism, one of its main interest is that it also lead Girard to discover the notion of linear function, which rapidly gave rise to linear logic. It is one of the originality of linear logic that its syntax was derived from its semantics.