Language peer sets for Edinburgh LCF:
Designed 1979 ↑
1970s languages ↑
High Cold War↑
alternate simple view
Country: United Kingdom
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.
Gordon, M.; Milner, R.; Wadsworth, C. (1979) Gordon, M.; Milner, R.; Wadsworth, C. "Edinburgh LCF: a mechanised logic of computation" LNCS 78 Springer-Verlag, 1979
Jacek Leszczylowski (1980) Jacek Leszczylowski "An Experiment with Edinburgh LCF", 5th Conference on Automated Deduction, Les Arcs, France, LNCS 87, 1980
Leszczylowski, Jacek (1980) Leszczylowski, Jacek "Edinburgh LCF Supporting FP-Systems", Springer, IFB 33, 1980
Leszczylowski, Jacek (1980) Leszczylowski, Jacek "On Proving Laws of the Algebra of FP-Systems in Edinburgh LCF", First Annual National Conference on Artificial Intelligence, Stanford, 1980
Leszczylowski, Jacek (1980) Leszczylowski, Jacek "Theory of FP-systems in Edinburgh LCF", Computer Science Department,Technical Reports, Edinburgh, Scotland, 1980
Leszczylowski, Jacek and I.Hansen (1980) Leszczylowski, Jacek and I.Hansen "Models of Microprograms", Proc. 13th Annual Workshop on Microprogramming, Colorado Springs, USA 1980
Leszczylowski, Jacek (1981) Leszczylowski, Jacek "FP-systems in Edinburgh LCF", Proc. of the International Colloquium on Formalization of Programming Concepts, Peniscola, Spain, LNCS 107, 1981
Cohn, A. (1982) Cohn, A. "The correctness of a predecence parsing algorithm in LCF." Technical Report No. 21, University of Cambridge, 1982.
Cohn, A. and Milner, R. (1982) 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
Cohn, Avra; Milner, Robin (1982) Cohn, Avra; Milner, Robin "On using Edinburgh LCF to prove the correctness of a parsing algorithm" Technical Report UCAM-CL-TR-20 February 1982
Online copy at UCAM
Cohn, A. (1983) Cohn, A. "The Equivalence of Two Semantic Definitions: A Case Study in LCF." SIAM Journal of Computing. May 1983.