, P-L. Curien 1 and T. Hardin 2 A. Rios 3 , 1CNRS and LIENS, 45, rud d'Ulm, Paris, France and 2INRA, Rocquencourt, and LITP, Universite Pierre et Marie Curie, case 168, 75252 ParisCedex 05, France 3Department of Computing Science, 17 Lilybank Gardens, University of Glasgow, GlasgowG12 8QQ, UK
[lambda][sigma]-calculus is an extended [lambda]-calculus where substitutions are handled explicitly. It is similar to, and inspired by, Categorical Combinatory logic (CCL). The strong normalization of [sigma], the subcalculus which computes substitutions, may be inferred from the strong normalization of the similar subsystem SUBST of CCL. We present here an independent proof of the termination of several substitution calculi, including [sigma] and SUBST.
: [lambda]-calculus, explicit substitutions, rewriting systems, normalization.
Part of the OUP Journal of Logic and Computation WWW service
Click here to register with OUP.
This page is maintained by OUP admin
Last updated 08 Jan 97
Part of the OUP Journals World Wide Web service.
Copyright Oxford University Press, 1997