Bibliografía

1
M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy.
Explicit Substitutions.
Journal of Functional Programming, 1(4):375-416, 1991.

2
M. Ayala-Rincón and F. Kamareddine.
Strategies for Simply-Typed Higher Order Unification via $ \lambda s_e$-Style of Explicit Substitution.
In R. Kennaway, editor, The Third International Workshop on Explicit Substitutions Theory and Applications to Programs and Proofs (WESTAPP 2000), Norwich, England, pages 3-17, July 2000.

3
M. Ayala-Rincón and F. Kamareddine.
Unification via $ \lambda s_e$-Style of Explicit Substitution.
In Second International Conference on Principles and Practice of Declarative Programming, Montreal, Canada, pages 163-174, September 2000.
Technical Report Higher Order Unification via $ \lambda s$-Style of Explicit Substitution, Computer and Electrical Engineering, Heriot-Watt University, Dec. 1999. Available at http://www.cee.hw.ac.uk/ultra.

4
Z.-el-A. Benaissa, P. Lescanne, and K. H. Rose.
Modeling Sharing and Recursion for Weak Reduction Strategies using Explicit Substitution.
In Programming Languages: Implementations, Logics and Programs PLILP'96, volume 1140 of LNCS, pages 393-407. Springer, 1996.

5
G. Dowek, T. Hardin, C. Kirchner, and F. Pfenning.
Unification via Explicit Substitutions: The Case of Higher-Order Patterns.
Rapport de Recherche 3591, INRIA, December 1998.

6
Gilles Dowek, Thérèse Hardin, and Claude Kirchner.
Higher-order Unification via Explicit Substitutions.
Information and Computation, 157(1/2):183-235, 2000.

7
W. Farmer.
A Unification Algorithm for Second-Order Monadic Terms.
Annals of Pure and Applied Logic, 39:131-174, 1988.

8
W. Goldfarb.
The Undecidability of the Second-Order Unification Problem.
Theoretical Computer Science, 13(2):225-230, 1981.

9
G. P. Huet.
A Unification Algorithm for Typed $ \lambda$-Calculus.
Theoretical Computer Science, 1:27-57, 1975.

10
F. Kamareddine and R. P. Nederpelt.
A useful $ \lambda$-notation.
Theoretical Computer Science, 155:85-109, 1996.

11
F. Kamareddine and A. Ríos.
Extending a $ \lambda$-calculus with Explicit Substitution which Preserves Strong Normalisation into a Confluent Calculus on Open Terms.
Journal of Functional Programming, 7:395-420, 1997.

12
C. Kirchner and C. Ringeiseen.
Higher-order Equational Unification via Explicit Substitutions.
In Proc. Algebraic and Logic Programming, volume 1298 of LNCS, pages 61-75. Springer, 1997.

13
L Magnusson.
The implementation of ALF - a proof editor based on Martin Löf's Type Theory with explicit substitutions.
PhD thesis, Chalmers, 1995.

14
C. Muñoz.
Proof-Term Synthesis on Dependent-Type Systems via Explicit Substitution.
Technical report, ICASE, Institute for Computer Applications in Science and Engineering, MS 132C, NASA Langley Research Center, Hampton, VA 23681-2199, USA, October 1999.

15
G. Nadathur and D. S. Wilson.
A representation of lambda terms suitable for operations on their intentions.
Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 341-348, 1990.

16
R. P. Nederpelt, J. H. Geuvers, and R. C. de Vrijer.
Selected papers on Automath.
North-Holland, Amsterdam, 1994.

17
C. Okasaki.
FUNCTIONAL PEARL Even Higher-Order Functions for Parsing or Why Would Anyone Ever Want to Use a Sixth-Order Function?
Journal of Functional Programming, 8(2):195-199, March 1999.

18
L. Paulson.
Isabelle: The next 700 Theorem Provers.
Logic and Computer Science, pages 361-386, 1990.

19
J. A. Robinson.
A Machine-oriented Logic Based on the Resolution Principle.
Journal of the ACM, 12(1):23-41, January 1965.