The semantics of second-order lambda calculus.(English)Zbl 0714.68052

The second-order lambda calculus, as a tool for solving problems connected with polymorphisms, can become important with respect to some programming languages. Because of its explicit lambda abstraction over types this calculus cannot be interpreted in the standard (naive) way, where terms denote functions and types sets of functions. The authors, inspired by some preceding ideas (Girard, Reynolds, McCracken, indeed Scott), define two model concepts: environmental model and combinatory model. The equivalence of both the models is proved as well as many other theorems and lemmas. A comparison with other models is given and some open problems are formulated.
Reviewer: P.Materna

MSC:

 68Q55 Semantics in the theory of computing 03B15 Higher-order logic; type theory (MSC2010) 68N15 Theory of programming languages