Editing Logic for Computable Functions (section)

{{Short description|1970s automated theorem prover}}
{{see also|Logic of Computable Functions}}
'''Logic for Computable Functions''' ('''LCF''') is an interactive [[automated theorem prover]] developed at [[Stanford University|Stanford]] and [[University of Edinburgh|Edinburgh]] by [[Robin Milner]] and collaborators in early 1970s, based on the theoretical foundation of [[Logic of Computable Functions|logic of computable functions]] previously proposed by [[Dana Scott]]. Work on the LCF system introduced the general-purpose [[programming language]] [[ML (programming language)|ML]] to allow users to write theorem-proving tactics, supporting [[algebraic data type]]s, [[parametric polymorphism]], [[abstract data types]], and [[Exception handling|exceptions]].