Using Fields and Explicit Substitutions to Implement Objects and Functions in a de Bruijn Setting

Abstract We propose a calculus of explicit substitutions with de Bruijn indices for implementing objects and functions which is confluent and preserves strong normalization. We start from Abadi and Cardelli’s ς-calculus [ 1 ] for the object calculus and from the λ ν -calculus [ 20 ] for the functional calculus. The de Bruijn setting poses problems when encoding the λ ν -calculus within the ς-calculus following the style proposed in [ 1 ]. We introduce fields as a primitive construct in the target calculus in order to deal with these difficulties. The solution obtained greatly simplifies the one proposed in [ 17 ] in a named variable setting. We also eliminate the conditional rules present in the latter calculus obtaining in this way a full non-conditional first order system.

Authors

• Eduardo Bonelli

Keywords

No keywords are indexed for this paper.