The Transformation Calculus and its Typing

Jacques Garrigue. In Proc. of the workshop on Type Theory and its Applications to Computer Systems, pages 34-45. Kyoto University RIMS Lecture Notes 851, July 1993.

Abstract. Many calculi supporting a notion of state have been proposed. However this notion is nearly always based on the intuition of a store, that is a binding from name to values. The exception, monads, recently focused on for I/Os, suffers from its rigidity.

The transformation calculus, an extension of lambda calculus, shows another, more general way to do that. It is different from others in that no orthogonal reduction rule is added to beta-reduction, but only structural ones.

We introduce here the transformation calculus, and give our approach to its typing. Fundamental properties, like confluence, have been shown, and two type systems, simple and polymorphic, are proposed.

You can get the dvi version of this paper tcalc.dvi.gz (31050 bytes), or the postscript one (72749 bytes).

JG 95.6.30