LCF: a history

LCF is an acronym for 'Logic of Computable Functions' (as developed by Dana Scott [ref] to facilitate reasoning about recursive functions) and was Robin Milnor's implementatiuon of its semantics supplimented by a lot of inovative computer engineering. It is one of the earlest examples (the other called PCHECK, written by Whit Diffie) of what people now call 'proof assistents' and at the time was thought of as such. None of the early systems of this genre were thought of as 'theorem provers'. To paraphrase John McCarthy “You can't expect a system to find a proof if you cannot even explicitly tell it the proof”.

Features

follow the manual - emphesizing function

Bibliography

MILNER - LCF Manual

Milner - MI 7

Scott, Dana

Weyhrauch - Japan

---