Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit substitutions. Journal of Functional Programming 1(4):375–416, October 1991.
Hassan Aït-Kaci. Warren's Abstract Machine: A Tutorial Reconstruction. Logic Programming Research Reports and Notes. MIT Press, Cambridge, MA, 1991.
Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2(3):297–347, 1992.
Peter B. Andrews. Resolution in type theory. Journal of Symbolic Logic 36:414–432, 1971.
Peter B. Andrews. General models, descriptions, and choice in type theory. Journal of Symbolic Logic 37:385–394, 1972.
Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory. Academic Press, ...