Artículo
Bonelli, E.; Rodriguez-Artalejo M.; Flum J. "Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting" (1999) 13th International Workshop on Computer Science Logic, CSL 1999 and held as International Workshops on Computer Science Logic, EACSL 1999. 1683:204-219
Consulte la política de Acceso Abierto del editor
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. © Springer-Verlag Berlin Heidelberg 1999.
Registro:
| Documento: | Artículo |
| Título: | Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting |
| Autor: | Bonelli, E.; Rodriguez-Artalejo M.; Flum J. |
| Filiación: | Laboratoire de Recherche en Informatique, Université de Paris-Sud, Orsay, 91405, France Departamento de Computación, Universidad de Buenos Aires, Argentina |
| Palabras clave: | Computer circuits; Reconfigurable hardware; Conditional rules; De Bruijn; De-Bruijn indices; Explicit Substitutions; First order systems; Functional calculus; Object calculi; Strong normalization; Calculations |
| Año: | 1999 |
| Volumen: | 1683 |
| Página de inicio: | 204 |
| Página de fin: | 219 |
| Título revista: | 13th International Workshop on Computer Science Logic, CSL 1999 and held as International Workshops on Computer Science Logic, EACSL 1999 |
| Título revista abreviado: | Lect. Notes Comput. Sci. |
| ISSN: | 03029743 |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v1683_n_p204_Bonelli |
Referencias:
- Abadi, M., Cardelli, L., (1996) A Theory of Objects, , Springer Verlag
- Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J., Explicit Substitutions (1991) Journal of Functional Programming, 4 (1), pp. 375-416
- Bloo, R., (1997) Preservation of Termination for Explicit Substitution, , PhD. Thesis, Eind- hoven University
- Bloo, R., Geuvers, H., Explicit Substitution: On the edge of strong normalization (1998) Theoretical Computer Science, p. 204
- Bloo, R., Rose, K., Combinatory Reduction Systems with explicit substitution that preserve strong normalization (1996) RTA’96, , LNCS 1103
- Bonelli, E., Using Fields and Explicit Substitutions to Implement Objects and Functions in a De Bruijn Setting, , ftp://ftp.lri.fr/LRI/articles/bonelli/objectdbfull.ps.gz, Full version obtainable by ftp at
- Briaud, D., An explicit eta rewrite rule (1995) Int. Conference on Typed Lambda Calculus and Applications, 902. , M.Dezani Ed., LNCS
- de Bruijn, N.G., Lambda calculus notation with nameless dummies, a tool for automatic formual manipulation with application to the Church-Rosser theorem (1972) Series A, Mathematical Sciences, 75, pp. 381-392. , Koninklijke Nederlandse Akademie van Wetenschappen
- Curien, P.-L., Hardin, T., Lévy, J.-J., (1991) Confluence Properties of Weak and Strong Calculi of Explicit Substitutions, , Technical Report, Centre d’Etudes et de Recherche en Informatique, CNAM
- Dershowitz, N., Orderings for term rewriting systems (1982) Theoretical Computer Science, 17 (3), pp. 279-301
- Ferreira, M., Kesner, D., Puel, L., Lambda-calculi with explicit substitutions and composition which preserve beta-strong normalization (1996) Proceedings of the 5Th International Conference on Algebraic and Logic Programming (ALP’96), p. 1139. , LNCS
- Hardin, T., (1987) Résultats De Confluence Pour Les règles Fortes De La Logique Combinatoire catégorique Et Liens Avec Les Lambda-Calculs, p. 4. , Thèse de doctorat, Université de Paris
- Hardin, T., Lévy, J.-J., A confluent calculus of substitutions (1989) France-Japan Artificial Intelligence and Computer Science Symposium
- Kamareddine, F., Ríos, A., A lambda calculus a la de Bruijn with Explicit Substitutions (1995) Proceedings of the 7Th International Symposium on Programming Languages, p. 982. , Implementations, Logics and Programs (PLILP’95), LNCS
- Kamareddine, F., Ríos, A., Extending a λ-calculus with Explicit Substitutions which Preserves Strong Normalization into a Confluent Calculus on Open Terms (1997) In Journal of Functional Programming, 7 (4)
- Kesner, D., Confluence properties of extensional and non-extensional lambda-calculi with explicit substitutions (1996) Proceedings of the 7Th International Conference on Rewriting Techniques and Applications (RTA’96), p. 1103. , LNCS
- Kesner, D., Martínez López, P.E., Explicit Substitutions for Objects and Functions (1998) Proceedings of the Joint International Symposiums: Programming Languages, Implementations, Logics and Program (PLILP’98) and Algebraic and Logic Programming (ALP), 1490, pp. 195-212. , LNCS
- Klop, J.W., (1980) Combinatory Reduction Systems, , PhD Thesis, University of Utrecht
- Klop, J.W., Term Rewriting Systems (1992) Handbook of Logic in Computer Science, 2. , S. Abramsky, D. Gabbay, and T.Maibaum, editors, Oxford University Press
- Lescanne, P., From λσ to λυ, a journey through calculi of explicit substitutions (1994) Ann. ACM Symp. on Principles of Programming Languages (POPL), pp. 60-69. , ACM
- Lescanne, P., Rouyer Degli, J., Explicit substitutions with de Bruijn’s levels (1995) RTA’95, , P.Lescanne editor, LNCS 914
- Melliès, P.A., Typed λ-calculi with explicit substitutions may not terminate (1995) TLCA’95, p. 902. , LNCS
- Muñoz, C.A., Confluence and Preservation of Strong Normalisation in an Explicit Substitutions Calculus (1996) Proceedings of the Eleven Annual IEEE Symposium on Logic in Computer Science
- Pagano, B., Des calculs de substitution explicit et leur application à la compilation des langages fonctionnels (1998) Université De Paris, p. 7. , Thèse de doctorat
- Ríos, A., (1993) Contribution à l’étude Des λ-calculs Avec Substitutions Explicites, p. 7. , Ph.D Thesis, Université de Paris
- Rose, K., Explicit Cyclic Substitutions (1992) CTRS’92, LNCS 656
- Takahashi, M., Parallel reduction in the λ-calculus (1989) Journal of Symbolic Computation, 7, pp. 113-123A4 - Comision Interministerial de Ciencia y Tecnologia (CICYT), MEC; Departamento Arquitectura de Computadores y Automatica (DACYA), UCM; Departamento Sistemas Informaticos y Programacion (DSIP), UCM; Escuela Superior de Informatica – UCM; Esprit Working Group EP 22457 (CCL II); et al.
Citas:
---------- APA ----------
Bonelli, E., Rodriguez-Artalejo M. & Flum J. (1999) . Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting. 13th International Workshop on Computer Science Logic, CSL 1999 and held as International Workshops on Computer Science Logic, EACSL 1999, 1683, 204-219.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v1683_n_p204_Bonelli [ ]
---------- CHICAGO ----------
Bonelli, E., Rodriguez-Artalejo M., Flum J. "Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting" . 13th International Workshop on Computer Science Logic, CSL 1999 and held as International Workshops on Computer Science Logic, EACSL 1999 1683 (1999) : 204-219.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v1683_n_p204_Bonelli [ ]
---------- MLA ----------
Bonelli, E., Rodriguez-Artalejo M., Flum J. "Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting" . 13th International Workshop on Computer Science Logic, CSL 1999 and held as International Workshops on Computer Science Logic, EACSL 1999, vol. 1683, 1999, pp. 204-219.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v1683_n_p204_Bonelli [ ]
---------- VANCOUVER ----------
Bonelli, E., Rodriguez-Artalejo M., Flum J. Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting. Lect. Notes Comput. Sci. 1999;1683:204-219.Available from: https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v1683_n_p204_Bonelli [ ]
