The semantics of second-order lambda calculus (Q751294)

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.