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
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
|