Volume 6: January - December 1996

Issue 6: December 1996


Strong normalization of substitutions

  • Strong normalization of substitutions
  • P-L. Curien1, T. Hardin2 and A. Rios3 1CNRS and LIENS, 45, rud d'Ulm, Paris, France, 2INRA, Rocquencourt, and LITP, Universite Pierre et Marie Curie, case 168, 75252 Paris Cedex 05, France and 3Department of Computing Science, 17 Lilybank Gardens, University of Glasgow, Glasgow G12 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.

    Keywords: [lambda]-calculus, explicit substitutions, rewriting systems, normalization.

    Pages: 799 - 817

    Part of the OUP Journal of Logic and Computation WWW service

    General Information

    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