Registro:

Referencias:

• Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J., Explicit substitutions (1991) Journal of Functional Programming, 1, pp. 375-416
• Abelson, H., Sussman, G., (1986) Structure and Interpretation of Computer Programs, , MIT Press
• Barendregt, H., (1984) The Lambda Calculus: Its Syntax and Semantics (Revised Edition), , North Holland
• 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
• Benaissa, Z., (1997) Les Calculs de Substitutions Explicites Comme Fondement de L'implantation des Langages Fonctionnels, , PhD thesis, Univ. Henri Poincare, Nancy
• Bloo, R., (1997) Preservation of Strong Normalization for Explicit Substitution, , PhD thesis, Department of Mathematics and Computing Science, Eindhoven University of Technology
• Bloo, R., Pure type systems with explicit substitutions (1999) Proceedings of FLOC'99 Workshop WESTAPP'99, pp. 45-58
• Bonelli, E., The polymorphic lambda calculus with explicit substitutions (1999) Proceedings of FLOC'99 Workshop WESTAPP'99, pp. 59-74
• 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
• 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
• 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
• Curien, P.-L., (1986) Categorical Combinators, Sequential Algorithms and Functional Programming, , Pitman, Revised edition : Birkhauser (1993)
• 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
• 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
• 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
• 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
• Goubault-Larrecq, J., (1997) A Proof of Weak Termination of the Simply Typed λσ-Calculus, , Technical report, INRIA, January
• Gordon, M.J.C., Melham, T.F., (1993) Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, , Cambridge University Press
• Guillaume, B., The λl-calculus (1999) Proceedings of FLOC'99 Workshop WESTAPP'99, pp. 2-13
• Guillaume, B., (1999) Un Calcul des Substitutions Avec Etiquettes, , PhD thesis, Université de Savoie, Chambéry
• Hardin, T., Lévy, J.-J., A confluent calculus of substitutions (1989) France-Japan Artificial Intelligence and Computer Science Symposium, , December
• Kamareddine, F., Nederpelt, R.P., On stepwise explicit substitution (1993) International Journal of Foundations of Computer Science, 4, pp. 197-240
• 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
• 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
• 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
• Kamareddine, F., Rios, A., (1999) Weak Normalization of the Simply Typed λSe-calculus, , Technical report, Heriot-Watt University, In preparation
• 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
• 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
• 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
• 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
• 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
• Magnusson, L., (1995) The Implementation of ALF - a Proof Editor Based on Martin Löf's Type Theory with Explicit Substitutions, , PhD thesis, Chalmers
• 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
• 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
• 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
• 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
• 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
• 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
• Nederpelt, R.P., Geuvers, J.H., De Vrijer, R.C., (1994) Selected Papers on Automath., , North-Holland, Amsterdam
• 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
• Paulson, L., Isabelle: The next 700 theorem provers (1990) Logic and Computer Science, pp. 361-386. , P. Odifreddi, ed., Academic Press
• Peyton-Jones, S.L., (1987) The Implementation of Functional Programming Languages, , Prentice-Hall
• Ríos, A., (1993) Contribution à L'étude des λ-Calculs Avec Substitutions Explicites, , PhD thesis, Université de Paris 7

Citas:

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

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

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

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