Registro:

Referencias:

• Abadi, M., Cardelli, L., Curien, P.L., Lévy, J.-J., Explicit substitutions (1991) Journal of Functional Programming, 4, pp. 375-416
• Barendregt, H., (1984) Studies in Logic and the Foundations of Mathematics, 103. , The Lambda Calculus; Its Syntax and Semantics. North-Holland. Revised edition
• Bognar, M., De Vrijer, R., The context calculus lambda-c (1999) Workshop on Logical Frameworks and Meta-languages (LFM), , Paris, France
• Bonelli, E., Kesner, D., Ríos, A., 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
• 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
• Bonelli, E., Kesner, D., Ríos, A., Relating higher-order and first-order rewriting (2005) Journal of Logic and Computation
• Baader, F., Nipkow, T., (1998) Term Rewriting and All That, , Cambridge University Press
• 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, H. Ganzinger, ed.. Springer-Verlag
• Breazu-Tannen, V., Combining algebra and higher order types (1988) 3rd Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 82-90. , IEEE Computer Society Press
• Curien, P.-L., (1993) Categorical Combinators, Sequential Algorithms and Functional Programming, , Progress in Theoretical Computer Science. Birkhaüser. Second edition
• Despeyroux, J., Felty, A., Hirschowitz, A., Higher-order abstract syntax in coq (1995) Technical Report, 2556. , INRIA, May
• 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
• Girard, J.-Y., Lafont, Y., Taylor, P., (1990) Proofs and Types, , Cambridge University Press
• 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
• Goguen, J., Thatcher, J., Wagner, E., An initial algebra approach to the specification, correctness and implementation of abstract data types (1978) Current Trends in Programming Methodology, 4, pp. 80-149. , Prentice Hall
• Huet, G., Oppen, D., Equations and rewrite rules: A survey (1980) Formal Language Theory: Perspectives and Open Problems, pp. 349-405. , R. V. Book, ed.. Academic Press
• Khasidashvili, Z., Expression reduction systems (1990) Proceedings of in Vekua Institute of Applied Mathematics, 36. , Tbilisi
• Klop, J.-W., (1980) Combinatory Reduction Systems, , PhD thesis, Mathematical Centre Tracts 127, CWI, Amsterdam
• Klop, J.-W., (1992) Term Rewriting Systems, 2. , Oxford University Press
• 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., Bridging de Bruijn indices and variable names in explicit substitutions calculi (1998) Logic Journal of the Interest Group of Pure and Applied Logic, 6, pp. 843-874
• 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
• Pfenning, F., Elliot, C., Higher-order abstract syntax (1988) ACM Symposium on Programming Language Design and Implementation, pp. 199-208. , ACM
• Pitts, A., Nominal logic, a first order theory of names and binding (2003) Information and Computation, 186, pp. 165-193
• Pollack, R., Closure under alpha-conversion (1993) Types for Proofs and Programs (TYPES), , H. Barendregt and T. Nipkow, eds. Number 806 in Lecture Notes in Computer Science, Nijmegen, The Netherlands
• Rose, K., Explicit cyclic substitutions (1992) Proceedings of the Third International Workshop on Conditional Term Rewriting Systems (CTRS), pp. 36-50. , M. Rusinowitch and J.-L. Rémy, eds.. Number 656 in Lecture Notes in Computer Science
• Rehof, J., Sørensen, M.H., The λΔ calculus (1994) Lecture Notes in Computer Science, pp. 516-542. , Theoretical Aspects of Computer Software (TACS), M. Hagiya and J. Mitchell, eds.. Number 789, Springer-Verlag
• (2003) Cambridge Tracts in Theoretical Computer Science, 55. , Term Rewriting Systems. Cambridge University Press, March
• 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., Weak orthogonality implies confluence: The higher-order case (1994) Lecture Notes in Computer Science, 813, pp. 379-392. , Proceedings of the 3rd International Symposium on Logical Foundations of Computer Science, A. Nerode and Y. Matiyasevich, eds. Springer-Verlag
• Van Raamsdonk, F., (1996) Confluence and Normalization for Higher-Order Rewriting, , PhD thesis, Amsterdam University, Netherlands
• Wolfram, D., (1993) Cambridge Tracts in Theoretical Computer Science, 21. , The Clausal Theory of Types Cambridge University Press

Citas:

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

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

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

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