Edinburgh LCF(ID:8177/)

Milner's "mechanisation" of Scott's LCF, which was (quoting the Turing Award citation), "probably the first theoretically based yet practical tool for machine-assisted proof construction."

There are two kinds of base variables and constants in LCF. Those that range over individuals
and those that range over truth values.
Related languages
LCF => Edinburgh LCF   Implementation of
Edinburgh LCF => Cambridge LCF   Evolution of
Edinburgh LCF => ML   Meta language for
Edinburgh LCF => PCF   Implementation
References:
  • Gordon, M.; Milner, R.; Wadsworth, C. "Edinburgh LCF: a mechanised logic of computation" LNCS 78 Springer-Verlag, 1979 view details
  • Jacek Leszczylowski "An Experiment with Edinburgh LCF", 5th Conference on Automated Deduction, Les Arcs, France, LNCS 87, 1980 view details
  • Leszczylowski, Jacek "Edinburgh LCF Supporting FP-Systems", Springer, IFB 33, 1980 view details
  • Leszczylowski, Jacek "On Proving Laws of the Algebra of FP-Systems in Edinburgh LCF", First Annual National Conference on Artificial Intelligence, Stanford, 1980 view details
  • Leszczylowski, Jacek "Theory of FP-systems in Edinburgh LCF", Computer Science Department,Technical Reports, Edinburgh, Scotland, 1980 view details
  • Leszczylowski, Jacek and I.Hansen "Models of Microprograms", Proc. 13th Annual Workshop on Microprogramming, Colorado Springs, USA 1980 view details
  • Leszczylowski, Jacek "FP-systems in Edinburgh LCF", Proc. of the International Colloquium on Formalization of Programming Concepts, Peniscola, Spain, LNCS 107, 1981 view details
  • Cohn, A. "The correctness of a predecence parsing algorithm in LCF." Technical Report No. 21, University of Cambridge, 1982. view details
  • Cohn, A. and Milner, R. "On using Edinburgh LCF to prove the correctness of a parsing algorithm." Technical Report CSR-113-82, University of Edinburgh, 1982 view details
  • Cohn, Avra; Milner, Robin "On using Edinburgh LCF to prove the correctness of a parsing algorithm" Technical Report UCAM-CL-TR-20 February 1982 view details External link: Online copy at UCAM
  • Cohn, A. "The Equivalence of Two Semantic Definitions: A Case Study in LCF." SIAM Journal of Computing. May 1983. view details