 Each of these accounts induces its own synonymy relation on the phrases of the programming language: in a nutshell, the full abstraction property states that the denotational and operational approaches define the same relation. This is a benchmark property for a semantical account of a programming language, and its failure for an intuitive denotational account of a simple language based on lambda-calculus has led eventually to refinements of the technical tools of denotational semantics culminating in game semantics, partly inspired by the dialogue games originally used in the semantics of intuitionistic logic by Lorenzen and his school, and later extended by Blass and others to the interpretation of Girard’s linear logic. This bridge between constructive logic and programming has also suggested stronger forms of relation between semantics and proof-theory, of which the notion of full completeness is perhaps the most remarkable instance. 