The weak normalization of the simply typed λse-calculus
In this paper, we show the weak normalization (WN) of the simply-typed λse-calculus with open terms where abstractions are decorated with types, and metavariables, de Bruijn indices and updating operators are decorated with environments. We show a proof of WN using the λωe-calculus, a calculus isomo...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | , |
| Formato: | Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
2007
|
| Acceso en línea: | Registro en Scopus DOI Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 04453caa a22004697a 4500 | ||
|---|---|---|---|
| 001 | PAPER-22698 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518205417.0 | ||
| 008 | 190411s2007 xx ||||fo|||| 00| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-34447562615 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 100 | 1 | |a Arbiser, A. | |
| 245 | 1 | 4 | |a The weak normalization of the simply typed λse-calculus |
| 260 | |c 2007 | ||
| 270 | 1 | 0 | |m Arbiser, A.; Department of Computer Science, University of Buenos Aires, Pabellón I, 1428 Buenos Aires, Argentina; email: arbiser@dc.uba.ar |
| 506 | |2 openaire |e Política editorial | ||
| 504 | |a Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J., Explicit Substitutions (1991) Journal of Functional Programming, 1 (4), pp. 375-416 | ||
| 504 | |a Benaissa, Z., Briaud, D., Lescanne, P., Rouyer-Degli, J., λν, a calculus of explicit substitutions which preserves strong normalisation (1996) Functional Programming, 6 (5) | ||
| 504 | |a P.-L. Curien. Categorical Combinators, Sequential Algorithms and Functional Programming. Pitman, 1986. Revised edition, Birkhäuser (1993); Curien, P.-L., Hardin, T., Lévy, J.-J., Confluence properties of weak and strong calculi of explicit substitutions (1617) Technical Report RR, , INRIA, Rocquencourt | ||
| 504 | |a de Bruijn, N., Lambda-Calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem (1972) Indag. Mat, 34 (5), pp. 381-392 | ||
| 504 | |a Goubault-Larrecq, J., A proof of weak termination of the simply typed λσ-calculus (1998) LNCS, 1512, pp. 134-151. , Proc. Int. Workshop on Types for Proofs and Programs TYPES'96 | ||
| 504 | |a Guillaume, B., (1999) Un calcul des substitutions avec étiquettes, , PhD thesis, Université de Savoie, Chambéry, France | ||
| 504 | |a Kamareddine, F., Ríos, A., Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms (1997) Journal of Functional Programming, 7 (4), pp. 395-420 | ||
| 504 | |a Kamareddine, F., Ríos, A., Relating the λσ- and λs-styles of explicit substitutions (2000) Logic and Computation, 10 (3), pp. 349-380 | ||
| 504 | |a Ríos, A., (1993) Contribution à l'étude des λ-calculs avec substitutions explicites, , PhD thesis, Université de Paris 7 | ||
| 520 | 3 | |a In this paper, we show the weak normalization (WN) of the simply-typed λse-calculus with open terms where abstractions are decorated with types, and metavariables, de Bruijn indices and updating operators are decorated with environments. We show a proof of WN using the λωe-calculus, a calculus isomorphic to λse→. This proof is strongly influenced by Goubault-Larrecq's proof of WN for the λσ-calculus but with subtle differences which show that the two styles require different attention. Furthermore, we give a new calculus λω′e which works like λse but which is closer to λσ than λωe. For both λωe and λω′e we prove WN for typed semi-open terms (i.e. those which allow term variables but no substitution variables), unlike the result of Goubault-Larrecq which covered all λσ open terms. © The Author, 2007. Published by Oxford University Press. All rights reserved. |l eng | |
| 593 | |a Department of Computer Science, University of Buenos Aires, Pabellón I, 1428 Buenos Aires, Argentina | ||
| 593 | |a School of Mathematical and Computer Sciences, Heriot-Watt University, Riccarton, Edinburgh EH14 4AS, United Kingdom | ||
| 690 | 1 | 0 | |a EXPLICIT SUBSTITUTION |
| 690 | 1 | 0 | |a LAMBDA CALCULUS |
| 690 | 1 | 0 | |a NORMALIZATION |
| 690 | 1 | 0 | |a SIMPLE TYPING |
| 700 | 1 | |a Kamareddine, F. | |
| 700 | 1 | |a Rios, A. | |
| 773 | 0 | |d 2007 |g v. 15 |h pp. 121-147 |k n. 2 |p Logic J. IGPL |x 13670751 |t Logic Journal of the IGPL | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-34447562615&doi=10.1093%2fjigpal%2fjzm003&partnerID=40&md5=b5b0ac87eff4b709b84cd661082ad8e3 |y Registro en Scopus |
| 856 | 4 | 0 | |u https://doi.org/10.1093/jigpal/jzm003 |y DOI |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_13670751_v15_n2_p121_Arbiser |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_13670751_v15_n2_p121_Arbiser |y Registro en la Biblioteca Digital |
| 961 | |a paper_13670751_v15_n2_p121_Arbiser |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/article |a info:ar-repo/semantics/artículo |b info:eu-repo/semantics/publishedVersion | ||
| 999 | |c 83651 | ||