Bibliography

Click here to get it.

Explicit Substitutions

P.-L. Curien, T. Hardin, J.-J. Lévy, Confluence properties of weak and strong calculi of explicit substitutions, J.A.C.M 1996

Automated Theorem Proving

G. Dowek, Th. Hardin, C. Kirchner, HOL lambda-sigma : an intentional first-order expression of higher-order logic
G. Dowek, Th. Hardin, C. Kirchner, Theorem proving modulo

Unification

G. Dowek, Th. Hardin, C. Kirchner, F. Pfenning, Higher-order unification via explicit substitutions: the case of higher-order patterns, M. Maher (Ed.), Joint international conference and symposium on logic programming (1996), pp. 259-273.
. Dowek, Th. Hardin, C. Kirchner, Higher-order unification via explicit substitutions, D. Kozen (Ed.), Logic in computer science (1995), pp. 366-374.