zbMATH — the first resource for mathematics

Explicitly typed \(\lambda\mu\)-calculus for polymorphism and call-by-value. (English) Zbl 0933.03009
Girard, Jean-Yves (ed.), Typed lambda calculi and applications. 4th international conference, TLCA ’99. L’Aquila, Italy, April 7–9, 1999. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1581, 162-176 (1999).
Summary: We introduce an explicitly typed \(\lambda\mu\)-calculus of call-by-value as a short-hand for the second-order Church-style. Our motivation comes from the observation that in Curry-style polymorphic calculi, control operators such as callcc or \(\mu\)-operators cannot, in general, treat the terms placed on the control operator’s left. Folloing the continuation semantics, we also discuss the notion of values in classical system, and propose an extended form of values. It is shown that the CPS-translation is sound with respect to \(\lambda 2\) (second-order \(\lambda\)-calculus). Next, we provide an explicitly and an implicitly typed Damas-Milner system with \(\mu\)-operators. Finally, we give a brief comparison with standard ML plus callcc, and discuss a natural way to avoid the unsoundness of ML with callcc.
For the entire collection see [Zbl 0911.00022].

03B40 Combinatory logic and lambda calculus
68N18 Functional programming and lambda calculus
03B70 Logic in computer science