-
- 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
-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
-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 -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 -Calculus.
Theoretical Computer Science, 1:27-57, 1975.
- 10
-
F. Kamareddine and R. P. Nederpelt.
A useful -notation.
Theoretical Computer Science, 155:85-109, 1996.
- 11
-
F. Kamareddine and A. Ríos.
Extending a -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.