The lambda sigma -calculus is a concrete lambda -calculus of explicit subst
itutions, designed for reasoning about implementations of lambda -calculi.
Higher-order abstract syntax is an approach to metaprogramming that explici
tly captures the variable-binding aspects of programming language construct
s. A new calculus of explicit substitutions for higher-order abstract synta
x is introduced, allowing a high-level description of variable binding in o
bject languages while also providing substitutions as explicit programmer-m
anipulable data objects. The new calculus is termed the lambda sigma beta (
0)-calculus, since it makes essential use of an extension of beta (0)-unifi
cation (described in another paper). Termination and confluence are verifie
d for the lambda sigma beta (0)-calculus similarly to that for the ncr-calc
ulus, and an efficient implementation is given in terms of first-order rena
ming substitutions. The verification of confluence makes use of a verified
adaptation of Nipkow's higher-order critical pairs lemma to the forms of re
write rules required for the statement of the lambda sigma beta (0)-calculu
s. (C) 2001 Academic Press.