Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting
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. Th...
Guardado en:
| Publicado: |
1999
|
|---|---|
| Materias: | |
| Acceso en línea: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v1683_n_p204_Bonelli http://hdl.handle.net/20.500.12110/paper_03029743_v1683_n_p204_Bonelli |
| Aporte de: |
| id |
paper:paper_03029743_v1683_n_p204_Bonelli |
|---|---|
| record_format |
dspace |
| spelling |
paper:paper_03029743_v1683_n_p204_Bonelli2023-06-08T15:28:19Z Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting Computer circuits Reconfigurable hardware Conditional rules De Bruijn De-Bruijn indices Explicit Substitutions First order systems Functional calculus Object calculi Strong normalization Calculations 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. © Springer-Verlag Berlin Heidelberg 1999. 1999 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v1683_n_p204_Bonelli http://hdl.handle.net/20.500.12110/paper_03029743_v1683_n_p204_Bonelli |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-134 |
| collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
| topic |
Computer circuits Reconfigurable hardware Conditional rules De Bruijn De-Bruijn indices Explicit Substitutions First order systems Functional calculus Object calculi Strong normalization Calculations |
| spellingShingle |
Computer circuits Reconfigurable hardware Conditional rules De Bruijn De-Bruijn indices Explicit Substitutions First order systems Functional calculus Object calculi Strong normalization Calculations Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting |
| topic_facet |
Computer circuits Reconfigurable hardware Conditional rules De Bruijn De-Bruijn indices Explicit Substitutions First order systems Functional calculus Object calculi Strong normalization Calculations |
| description |
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. © Springer-Verlag Berlin Heidelberg 1999. |
| title |
Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting |
| title_short |
Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting |
| title_full |
Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting |
| title_fullStr |
Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting |
| title_full_unstemmed |
Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting |
| title_sort |
using fields and explicit substitutions to implement objects and functions in a de bruijn setting |
| publishDate |
1999 |
| url |
https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v1683_n_p204_Bonelli http://hdl.handle.net/20.500.12110/paper_03029743_v1683_n_p204_Bonelli |
| _version_ |
1768542788918444032 |