TY - GEN
T1 - Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting
AU - Bonelli, Eduardo
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1999.
PY - 1999
Y1 - 1999
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84956864562&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84956864562&partnerID=8YFLogxK
U2 - 10.1007/3-540-48168-0_15
DO - 10.1007/3-540-48168-0_15
M3 - Conference contribution
AN - SCOPUS:84956864562
SN - 3540665366
SN - 9783540665366
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 204
EP - 219
BT - Computer Science Logic - 13th International Workshop, CSL 1999 - 8th Annual Conference of the EACSL, Proceedings
A2 - Flum, Jörg
A2 - Rodriguez-Artalejo, Mario
T2 - 13th International Workshop on Computer Science Logic, CSL 1999 and held as International Workshops on Computer Science Logic, EACSL 1999
Y2 - 20 September 1999 through 25 September 1999
ER -