Registro:

Referencias:

• Abadi, M., Cardelli, L., Curien, P.L., Lévy, J.-J., Explicit substitutions (1991) Journal of Functional Programming, 4, pp. 375-416
• Arts, T., Giesl, J., Termination of term rewriting using dependency pairs (2000) Theoretical Computer Science, 236, pp. 133-178
• Barendregt, H., The Lambda Calculus: Its Syntax and Semantics (1984) Studies in Logic and the Foundations of Mathematics, 103. , North-Holland. Revised Edition
• Benaissa, Z.-E.-A., Briaud, D., Lescanne, P., Rouyer-Degli, J., λv, a calculus of explicit substitutions which preserves strong normalisation (1996) Journal of Functional Programming, 6, pp. 699-722
• Bachmair, L., Dershowitz, N., Critical pair criteria for completion (1988) Journal of Symbolic Computation, 6, pp. 1-18
• Bloo, R., (1997) Preservation of Termination for Explicit Substitution, , PhD thesis, Eindhoven University of Technology
• Bloo, R., Rose, K., Preservation of strong normalization in named lambda calculi with explicit substitution and garbage collection (1995) Computing Science in the Netherlands, pp. 62-72. , Netherlands Computer Science Research Foundation
• Bloo, R., Rose, K., Combinatory reduction systems with explicit substitution that preserve strong normalisation (1996) Lecture Notes in Computer Science, 1103. , 7th International Conference on Rewriting Techniques and Applications, New Brunswick, NJ, USA. H. Ganzinger, ed, Springer-Verlag
• Bonelli, E., Kesner, D., ARíos, A de Bruijn notation for higher-order rewriting (2000) Lecture Notes in Computer Science, 1833, pp. 62-79. , 11th International Conference on Rewriting Techniques and Applications, L. Bachmair, ed. Springer-Verlag, July
• Bonelli, E., Kesner, D., Ríos, A., From higher-order to first-order rewriting (extended abstract) (2001) Lecture Notes in Computer Science, 2051, pp. 47-62. , 12th International Conference on Rewriting Techniques and Applications, A. Middeldorp, ed., Springer-Verlag, May
• Bonelli, E., Kesner, D., Ríos, A., De Bruijn indices for Metaterms (2005) Journal of Logic and Computation, 15, pp. 857-902
• Bonelli, E., A normalization result for higher-order calculi with explicit substitutions (2003) Lecture Notes in Computer Science, 2626, pp. 153-168. , Foundations of Software Science and Computation Structures, A. Gordon, ed. Springer-Verlag
• Bonelli, E., (2001) Substitutions Explicites et Réécriture de Termes, , Thèse de doctorat, Université Paris XI, Orsay, November
• Briaud, D., An explicit eta rewrite rule (1995) Lecture Notes in Computer Science, 902, pp. 94-108. , Proceedings of the 2nd International Conference of Typed Lambda Calculus and Applications, M. Dezani-Ciancaglini and G. Plotkin, eds, Springer-Verlag
• Dershowitz, N., Orderings for term rewriting systems (1982) Theoretical Computer Science, 17, pp. 279-301
• David, R., Guillaume, B., The λl-calculus (1999) Proceedings of the 2nd Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs, pp. 2-13. , D. Kesner, ed., July
• Dowek, G., Hardin, T., Kirchner, C., Higher-order unification via explicit substitutions (1995) Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science (LICS), , D. Kozen, ed., San Diego, USA
• Dowek, G., Hardin, T., Kirchner, C., Theorem proving modulo (1998) Technical Report, RR 3400. , INRIA
• Dowek, G., Hardin, T., Kirchner, C., Unification via explicit substitutions: The case of higher-order patterns (1998) Technical Report, RR3591. , INRIA, December
• Dowek, G., Hardin, T., Kirchner, C., Higher-order unification via explicit substitutions (2000) Information and Computation, 157, pp. 183-235
• Dowek, G., Hardin, T., Kirchner, C., Hol-lambda-sigma: An intentional first-order expression of higher-order logic (2001) Mathematical Structures in Computer Science, 11, pp. 1-25
• Goubault-Larrecq, J., A proof of weak termination of typed lambda sigma-calculi (1998) Lecture Notes in Computer Science, 1512, pp. 134-151. , Proceedings of the International Workshop Types for Proofs and Programs, T. Altenkirch, W. Naraschewski, and B. Reus, eds, Springer-Verlag
• Gabbay, M., Pitts, A., A new approach to abstract syntax involving binders (1999) 14th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 214-224. , G. Longo, ed. IEEE Computer Society Press
• Hardin, T., n-reduction for explicit substitutions (1992) Lecture Notes in Computer Science, , Algebraic and Logic Programming'92, number 632
• Hardin, T., Lévy, J.-J., A confluent calculus of substitutions (1989) France-Japan Artificial Intelligence and Computer Science Symposium, , Izu (Japan)
• Jay, C.B., Ghani, N., The virtues of eta-expansion (1992) Technical Report, ECS-LFCS-92-243. , LFCS, University of Edimburgh
• Jay, C.B., Ghani, N., The virtues of eita-expansion (1995) Journal of Functional Programming, 5, pp. 135-154
• Jouannaud, J.-P., Rubio, A., The higher-order recursive path ordering (1999) Fourteenth Annual IEEE Symposium on Logic in Computer Science, , Trento, Italy
• Kesner, D., Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (1996) Lecture Notes in Computer Science, 1103, pp. 184-199. , 7th International Conference on Rewriting Techniques and Applications, New Brunswick, NJ, USA. H. Ganzinger, ed., Springer-Verlag
• Kesner, D., Confluence of extensional and non-extensional lambda-calculi with explicit substitutions (2000) Theoretical Computer Science, 238, pp. 183-220
• Khasidashvili, Z., Expression reduction systems (1990) Proceedings of in Vekua Institute of Applied Mathematics, 36. , Tbilisi
• Kamin, S., Lévy, J.-J., Attempts for generalizing the recursive path orderings (1980) Handwritten Paper, , University of Illinois
• Klop, J.-W., (1980) Combinatory Reduction Systems, , PhD thesis, Mathematical Centre Tracts 127, CWI, Amsterdam
• Khasidashvili, Z., Ogawa, M., Van Oostrom, V., Perpetuality and uniform normalization in orthogonal rewrite systems (2001) Information and Computation, 164, pp. 118-151
• 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 the 7th International Symposium on Proceedings of the International Symposium on Programming Language Implementation and Logic Programming, D. Swierstra and M. Hermenegildo, eds, Springer-Verlag, September
• Klop, J.-W., Van Oostrom, V., Van Raamsdonk, F., Combinatory reduction systems: Introduction and survey (1993) Theoretical Computer Science, 121, pp. 279-308
• Melliès, P.-A., (1996) Description Abstraite des Systèmes de Réécriture, , PhD thesis, Université Paris VII
• Melliès, P.-A., Axiomatic rewriting theory II: The lambda-sigma calculus enjoys finite normalisation cones (2000) Journal of Logic and Computation, 10, pp. 461-487
• Miller, D., A logic programming language with lambda-abstraction, function variables, and simple unification (1991) Journal of Logic and Computation, 1, pp. 497-536
• Muñoz, C., A left-linear variant of λσ (1997) Lecture Notes in Computer Science, 1298. , Proceedings of the 6th International Conference on Algebraic and Logic Programming (ALP'97), M. Hanus, J. Heering, and K. Meinke, eds., Springer-Verlag
• Muñoz, C., Dependent types and explicit substitutions: A meta-theoretical development (2001) Mathematical Structures in Computer Science, 11
• Nipkow, T., Higher-order critical pairs (1991) 6th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 342-349. , IEEE Computer Society Press
• Pagano, B., (1998) Des Calculs de Substitution Explicite et de Leur Application À la Compilation des Langages Fonctionnels, , Thèse de doctorat, Université Pierre et Marie Curie
• Pitts, A., Nominal logic, a first order theory of names and binding (2003) Information and Computation, 186, pp. 165-193
• Ríos, A., (1993) Contribution À L'étude des λ-Calculus Avec Substitutions Explicites, , Thèse de doctorat, Université de Paris VII
• Rose, K., Explicit cyclic substitutions (1992) Lecture Notes in Computer Science, 656, pp. 36-50. , Proceedings of the Third International Workshop on Conditional Term Rewriting Systems (CTRS), M. Rusinowitch and J.-L. Rémy, eds, Springer-Verlag
• Stehr, M.-O., CINNI-a generic calculus of explicit substitutions and its application to λ-, ς-and π-Calculi (2001) Electronic Notes in Theoretical Computer Science, 36. , K. Futatsugi, ed. Elsevier
• Urban, C., Pitts, A., Gabbay, M., Nominal unification (2004) Theoretical Computer Science
• Van Oostrom, V., (1994) Confluence for Abstract and Higher-order Rewriting, , PhD thesis, Vrije University, Amsterdam, Netherlands
• Van Oostrom, V., Van Raamsdonk, F., Comparing Combinatory reduction systems and higher-order rewrite systems (1994) Lecture Notes in Computer Science, 816, pp. 276-304. , 1st International Workshop on Higher-Order Algebra, Logic, and Term Rewriting, J. Heering, K. Meinke, B. Möller, and T. Nipkow, eds, Springer-Verlag. Selected Papers
• Van Raamsdonk, F., (1996) Confluence and Normalization for Higher-Order Rewriting, , PhD thesis, Amsterdam University, Netherlands
• Zantema, H., Termination of term rewriting by semantic labelling (1995) Fundamenta Informaticae, 24, pp. 89-105

Citas:

---------- APA ----------

---------- CHICAGO ----------

---------- MLA ----------

---------- VANCOUVER ----------