Relating the λσ- and λs-styles of explicit substitutions
Two methods of explicit substitutions, λσ- and λs-styles, are compared. A criterion of adequacy is used to simulate β-reduction in calculi of explicit substitutions and apply it to several calculi: λσ; λσ↑; λv; λs; λt; and λu. Results proved that λt is more adequate than λv and that λu is more adequ...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | |
| Formato: | Acta de conferencia Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
Oxford Univ Press
2000
|
| Acceso en línea: | Registro en Scopus DOI Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 10663caa a22009017a 4500 | ||
|---|---|---|---|
| 001 | PAPER-2347 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518203144.0 | ||
| 008 | 190411s2000 xx ||||fo|||| 00| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-1642586649 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 030 | |a JLCOE | ||
| 100 | 1 | |a Kamareddine, F. | |
| 245 | 1 | 0 | |a Relating the λσ- and λs-styles of explicit substitutions |
| 260 | |b Oxford Univ Press |c 2000 | ||
| 270 | 1 | 0 | |m Kamareddine, Fairouz; Heriot-Watt Univ, Scotland, United Kingdom |
| 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, pp. 375-416 | ||
| 504 | |a Abelson, H., Sussman, G., (1986) Structure and Interpretation of Computer Programs, , MIT Press | ||
| 504 | |a Barendregt, H., (1984) The Lambda Calculus: Its Syntax and Semantics (Revised Edition), , North Holland | ||
| 504 | |a Benaissa, Z., Briaud, D., Lescanne, P., Rouyer-Degli, J., λυ, a calculus of explicit substitutions which preserves strong normalization (1996) Journal of Functional Programming, 6, pp. 699-722 | ||
| 504 | |a Benaissa, Z., (1997) Les Calculs de Substitutions Explicites Comme Fondement de L'implantation des Langages Fonctionnels, , PhD thesis, Univ. Henri Poincare, Nancy | ||
| 504 | |a Bloo, R., (1997) Preservation of Strong Normalization for Explicit Substitution, , PhD thesis, Department of Mathematics and Computing Science, Eindhoven University of Technology | ||
| 504 | |a Bloo, R., Pure type systems with explicit substitutions (1999) Proceedings of FLOC'99 Workshop WESTAPP'99, pp. 45-58 | ||
| 504 | |a Bonelli, E., The polymorphic lambda calculus with explicit substitutions (1999) Proceedings of FLOC'99 Workshop WESTAPP'99, pp. 59-74 | ||
| 504 | |a Bloo, R., Rose, K., Combinatory reduction systems with explicit substitution that preserve strong normalization (1996) Lecture Notes in Computer Science, 1103. , Proceedings of RTA '96', Springer-Verlag | ||
| 504 | |a Curien, P.-L., Hardin, T., Lévy, J.-J., Confluence properties of weak and strong calculi of explicit substitutions (1996) Journal of the ACM, 43, pp. 362-397 | ||
| 504 | |a Constable, R.L., Allen, S., Bromley, H., Cleaveland, W., Cramer, F., Harper, R., Howe, D., Smith, S., (1986) Implementing Mathematics with the NUPRL Development System, , Prentice-Hall | ||
| 504 | |a Curien, P.-L., (1986) Categorical Combinators, Sequential Algorithms and Functional Programming, , Pitman, Revised edition : Birkhauser (1993) | ||
| 504 | |a De Bruijn, N.G., Lambda-Calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem (1972) Indagationes Mathematicae, 34, pp. 381-392 | ||
| 504 | |a De Bruijn, N.G., (1978) A Namefree Lambda Calculus with Facilities for Internal Definition of Expressions and Segments, , Technical Report TH-Report 78-WSK-03, Department of Mathematics, Eindhoven University of Technology | ||
| 504 | |a Dowek, G., Hardin, T., Kirchner, C., Higher order unification via explicit substitutions (1995) Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pp. 366-374. , San Diego | ||
| 504 | |a Ferreira, M.C.F., Kesner, D., Puel, L., λ-calculi with explicit substitutions preserving strong normalization (1999) Applicable Algebra in Engineering, Communication and Computation, 9, pp. 333-371 | ||
| 504 | |a Goubault-Larrecq, J., (1997) A Proof of Weak Termination of the Simply Typed λσ-Calculus, , Technical report, INRIA, January | ||
| 504 | |a Gordon, M.J.C., Melham, T.F., (1993) Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, , Cambridge University Press | ||
| 504 | |a Guillaume, B., The λl-calculus (1999) Proceedings of FLOC'99 Workshop WESTAPP'99, pp. 2-13 | ||
| 504 | |a Guillaume, B., (1999) Un Calcul des Substitutions Avec Etiquettes, , PhD thesis, Université de Savoie, Chambéry | ||
| 504 | |a Hardin, T., Lévy, J.-J., A confluent calculus of substitutions (1989) France-Japan Artificial Intelligence and Computer Science Symposium, , December | ||
| 504 | |a Kamareddine, F., Nederpelt, R.P., On stepwise explicit substitution (1993) International Journal of Foundations of Computer Science, 4, pp. 197-240 | ||
| 504 | |a Kamareddine, F., Ríos, A., A λ-calculus à la de Bruijn with explicit substitutions (1995) Lecture Notes in Computer Science, 982, pp. 45-62. , Proceedings of Programming Languages Implementation and the Logic of Programs PULP'95, Springer-Verlag | ||
| 504 | |a Kamareddine, F., Ríos, A., Extending a λ-calculus with explicit substitution which preserves strong normalization into a confluent calculus on open terms (1997) Journal of Functional Programming, 7, pp. 395-420 | ||
| 504 | |a Kamareddine, F., Ríos, A., Bridging de Bruijn indices and variable names in explicit substitutions calculi (1998) The Logic Journal of the Interest Group of Pure and Applied Logic, IGPL, 6, pp. 843-874 | ||
| 504 | |a Kamareddine, F., Rios, A., (1999) Weak Normalization of the Simply Typed λSe-calculus, , Technical report, Heriot-Watt University, In preparation | ||
| 504 | |a Kamareddine, F., Ríos, A., Wells, J.B., Calculi of generalised βe-reduction and explicit substitution: Type free and simply typed versions (1998) Journal of Functional and Logic Programming, pp. 1-44 | ||
| 504 | |a Lescanne, P., From λσ to λυ, a journey through calculi of explicit substitutions (1994) Proceedings of the 21st Annual ACM Symposium on Principles of Programming Languages, Portland (OR, USA), pp. 60-69. , Hans Boehm, ed., ACM | ||
| 504 | |a Lawall, J.L., Mairson, H., Optimality and inefficiency: What isn't a cost model of the lambda calculus? (1996) Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming, pp. 92-101 | ||
| 504 | |a Lang, F., Rose, K., Two calculi of explicit substitution with confluence on metaterms and preservation of strong normalization (1998) Proceedings of RTA Workshop WESTAPP'98 | ||
| 504 | |a Lescanne, P., Rouyer-Degli, J., Explicit substitutions with de Bruijn's levels (1995) Lecture Notes in Computer Science, 914, pp. 294-308. , Proceedings 6th Conference on Rewriting Techniques and Applications, Kaiserslautern (Germany), J. Hsiang, ed. Springer-Verlag | ||
| 504 | |a Magnusson, L., (1995) The Implementation of ALF - a Proof Editor Based on Martin Löf's Type Theory with Explicit Substitutions, , PhD thesis, Chalmers | ||
| 504 | |a Melliès, P.-A., Typed λ-calculi with explicit substitutions may not terminate (1995) Lecture Notes in Computer Science, 902. , Proceedings of Typed Lambda Calculi and Application: TLCA'95, Springer-Verlag | ||
| 504 | |a Muñoz, C., Proof representation in type theory: State of the art (1996) Proceedings of the XXII Latin-American Conference of Informatics CLEI Panel 96, , Santafé de Bogotá, Colombia, June | ||
| 504 | |a Muñoz, C., (1997) A Calculus of Substitutions for Incomplete-proof Representation in Type Theory, , Technical Report RR-3309, Unité de recherche INRIA-Rocquencourt, Novembre | ||
| 504 | |a Muñoz, C., Dependent types with explicit substitutions: A meta-theoretical development (1997) Lecture Notes in Computer Science, 1512, pp. 294-316. , Types for Proofs and Programs, Proceedings of the International Workshop TYPES'96 | ||
| 504 | |a Muñoz, C., (1997) Un Calcul de Substitutions Pour la Représentation de Preuves Partielles en Théorie de Types, , Thèse de doctorat, Université Paris 7, English version is available as an INRIA research report number RR-3309 | ||
| 504 | |a Muñoz, C., Proof synthesis via explicit substitutions on open terms (1998) Proceedings of International Workshop on Explicit Substitutions, Theory and Applications, WESTAPP 98, , Tsukuba (Japan), April | ||
| 504 | |a Nederpelt, R.P., Geuvers, J.H., De Vrijer, R.C., (1994) Selected Papers on Automath., , North-Holland, Amsterdam | ||
| 504 | |a Nadathur, G., Wilson, D., A representation of lambda terms suitable for operations on their intentions (1990) Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pp. 341-348 | ||
| 504 | |a Paulson, L., Isabelle: The next 700 theorem provers (1990) Logic and Computer Science, pp. 361-386. , P. Odifreddi, ed., Academic Press | ||
| 504 | |a Peyton-Jones, S.L., (1987) The Implementation of Functional Programming Languages, , Prentice-Hall | ||
| 504 | |a Ríos, A., (1993) Contribution à L'étude des λ-Calculs Avec Substitutions Explicites, , PhD thesis, Université de Paris 7 | ||
| 520 | 3 | |a Two methods of explicit substitutions, λσ- and λs-styles, are compared. A criterion of adequacy is used to simulate β-reduction in calculi of explicit substitutions and apply it to several calculi: λσ; λσ↑; λv; λs; λt; and λu. Results proved that λt is more adequate than λv and that λu is more adequate that λv, λσ↑, and λs. Counterexamples is given to show that all other comparisons are impossible according to the criterion. |l eng | |
| 536 | |a Detalles de la financiación: Engineering and Physical Sciences Research Council, GR/L36963, GR/L15685 | ||
| 536 | |a Detalles de la financiación: The authors are grateful for useful feedback and discussions with Roel Bloo, Jan Willem Klop and Pierre Lescanne. This work is supported by EPSRC grants number GR/L15685 and GR/L36963. | ||
| 593 | |a Dept. of Comp. and Elec. Engineering, Heriot-Watt University, Riccarton, Edinburgh EH14 4AS, United Kingdom | ||
| 593 | |a Department of Computer Science, University of Buenos Aires, Pabellón I - Cd. Univ., 1428 Buenos Aires, Argentina | ||
| 690 | 1 | 0 | |a THEOREM PROVING |
| 690 | 1 | 0 | |a EXPLICIT SUBSTITUTIONS |
| 690 | 1 | 0 | |a DIFFERENTIATION (CALCULUS) |
| 700 | 1 | |a Rìos, A. | |
| 711 | 2 | |c Oxford | |
| 773 | 0 | |d Oxford Univ Press, 2000 |g v. 10 |h pp. 349-380 |k n. 3 |p J Logic Comput |x 0955792X |t Journal of Logic and Computation | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-1642586649&doi=10.1093%2flogcom%2f10.3.349&partnerID=40&md5=d226a33adc45e0bcfcaab37b6651b0a7 |y Registro en Scopus |
| 856 | 4 | 0 | |u https://doi.org/10.1093/logcom/10.3.349 |y DOI |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_0955792X_v10_n3_p349_Kamareddine |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_0955792X_v10_n3_p349_Kamareddine |y Registro en la Biblioteca Digital |
| 961 | |a paper_0955792X_v10_n3_p349_Kamareddine |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 63300 | ||