TY - JOUR
T1 - Higher-order substitutions
AU - Duggan, Dominic
PY - 2001/1/10
Y1 - 2001/1/10
N2 - The λσ-calculus is a concrete λ-calculus of explicit substitutions, designed for reasoning about implementations of λ-calculi. Higher-order abstract syntax is an approach to metaprogramming that explicitly captures the variable-binding aspects of programming language constructs. A new calculus of explicit substitutions for higher-order abstract syntax is introduced, allowing a high-level description of variable binding in object languages while also providing substitutions as explicit programmer-manipulable data objects. The new calculus is termed the λσβ0-calculus, since it makes essential use of an extension of β0-unification (described in another paper). Termination and confluence are verified for the λσβ0-calculus similarly to that for the λσ-calculus, and an efficient implementation is given in terms of first-order renaming substitutions. The verification of confluence makes use of a verified adaptation of Nipkow's higher-order critical pairs lemma to the forms of rewrite rules required for the statement of the λσβ0-calculus.
AB - The λσ-calculus is a concrete λ-calculus of explicit substitutions, designed for reasoning about implementations of λ-calculi. Higher-order abstract syntax is an approach to metaprogramming that explicitly captures the variable-binding aspects of programming language constructs. A new calculus of explicit substitutions for higher-order abstract syntax is introduced, allowing a high-level description of variable binding in object languages while also providing substitutions as explicit programmer-manipulable data objects. The new calculus is termed the λσβ0-calculus, since it makes essential use of an extension of β0-unification (described in another paper). Termination and confluence are verified for the λσβ0-calculus similarly to that for the λσ-calculus, and an efficient implementation is given in terms of first-order renaming substitutions. The verification of confluence makes use of a verified adaptation of Nipkow's higher-order critical pairs lemma to the forms of rewrite rules required for the statement of the λσβ0-calculus.
UR - http://www.scopus.com/inward/record.url?scp=0035835296&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0035835296&partnerID=8YFLogxK
U2 - 10.1006/inco.2000.2887
DO - 10.1006/inco.2000.2887
M3 - Review article
AN - SCOPUS:0035835296
SN - 0890-5401
VL - 164
SP - 1
EP - 53
JO - Information and Computation
JF - Information and Computation
IS - 1
ER -