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...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Bonelli, E., Rodriguez-Artalejo M., Flum J.
Formato: SER
Materias:
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_03029743_v1683_n_p204_Bonelli
Aporte de:
id todo:paper_03029743_v1683_n_p204_Bonelli
record_format dspace
spelling todo:paper_03029743_v1683_n_p204_Bonelli2023-10-03T15:18:51Z Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting Bonelli, E. Rodriguez-Artalejo M. Flum J. 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. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar 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
Bonelli, E.
Rodriguez-Artalejo M.
Flum J.
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.
format SER
author Bonelli, E.
Rodriguez-Artalejo M.
Flum J.
author_facet Bonelli, E.
Rodriguez-Artalejo M.
Flum J.
author_sort Bonelli, E.
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
url http://hdl.handle.net/20.500.12110/paper_03029743_v1683_n_p204_Bonelli
work_keys_str_mv AT bonellie usingfieldsandexplicitsubstitutionstoimplementobjectsandfunctionsinadebruijnsetting
AT rodriguezartalejom usingfieldsandexplicitsubstitutionstoimplementobjectsandfunctionsinadebruijnsetting
AT flumj usingfieldsandexplicitsubstitutionstoimplementobjectsandfunctionsinadebruijnsetting
_version_ 1807323240781053952