zbMATH — the first resource for mathematics

Le lambda-calcul du second ordre. (The second-order lambda-calculus). (French) Zbl 0645.03013
Sémin. Bourbaki, 39ème année, Vol. 1986/87, Exp. No. 678, Astérisque 152/153, 173-185 (1987).
[For the entire collection see Zbl 0627.00006.]
This paper is in fact a detailed presentation of a typed \(\lambda\)- calculus denoted by F and introduced by the author in Proc. 2nd Scand. Logic Symp. 1970, Stud. Logic Found. Math. 63, 63-92 (1971; Zbl 0221.02013). It is a second order language since the abstraction operation is also defined on types. Its syntax is clear and simple and it has other “nice” properties (conversion rules and normal forms for terms, good expressive power) which makes it easy to manipulate. The type inference problem seems to be hard, and F has not yet an operational semantics. Future research is also dir- devoted mainly to ultrafilters - has since appeared: ibid. 127, 521-545 (1988).
Reviewer: E.Hartová

03B40 Combinatory logic and lambda calculus
68Q65 Abstract data types; algebraic specification
Full Text: Numdam EuDML