Explicitly typed λµcalculus for polymorphism and call-by-value

Abstract

We introduce an explicitly typed λ µcalculus of call-by-value as a short-hand for the 2nd order Church-style. Our motivation comes from the observation that in Curry-style polymorphic calculi, control operators such as callcc or -operators µcannot, in general, treat the terms placed on the control operator’s left. Following 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 λ2 (2nd order λ calculus). Next, we provide an explicitly and an implicitly typed Damas-Milner systems with µ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.