NOTE: The proof engine of ALF is written in SML, and the window interface is done by interviews.
Altenkirch, T. and Gaspes, V. and Nordstr\"{o}m B. and von Sydow B, "A User's guide to ALF". Available by FTP.
Coquand, T. "Pattern Matching with Dependent Types", Proceeding from the logical framework workshop at B\aa stad, June 1992, pp 66-79.
Magnusson, L. and Nordstr\"{o}m, B., "The ALF proof editor and its proof engine" In Types for Proofs and Programs, LNCS Vol 806, Nijmegen, 1994, pp 213-237.
Magnusson, L. "The implementation of ALF - a proof editor based on Martin-L\"{o}f's monomorhic type theory with explicit substitution", Ph.D thesis, to appear fall 1994.
Magnusson, L., "Refinement and local undo in the interactive proof editor ALF", The Informal Proceeding of the 1993 Workshop on Types for Proofs and Programs, Nijmegen 1993, pp 227-244.
Magnusson, L., "The new Implementation of ALF", The Informal proceeding from the logical framework workshop at B\aa stad, June 1992, pp 265-282.
Nordstr\"{o}m, B., "The ALF proof editor", The Informal Proceeding of the 1993 Workshop on Types for Proofs and Programs, Nijmegen 1993, pp 285-298.