Logic for Computable Functions
Logic for Computable Functions (LCF) is an interactive automated theorem prover developed at Stanford and Edinburgh by Robin Milner and collaborators in early 1970s, based on the theoretical foundation of logic of computable functions previously proposed by Dana Scott. Work on the LCF system introduced the general-purpose programming language ML to allow users to write theorem-proving tactics, supporting algebraic data types, parametric polymorphism, abstract data types, and exceptions.
- Comment
- enLogic for Computable Functions (LCF) is an interactive automated theorem prover developed at Stanford and Edinburgh by Robin Milner and collaborators in early 1970s, based on the theoretical foundation of logic of computable functions previously proposed by Dana Scott. Work on the LCF system introduced the general-purpose programming language ML to allow users to write theorem-proving tactics, supporting algebraic data types, parametric polymorphism, abstract data types, and exceptions.
- Has abstract
- enLogic for Computable Functions (LCF) is an interactive automated theorem prover developed at Stanford and Edinburgh by Robin Milner and collaborators in early 1970s, based on the theoretical foundation of logic of computable functions previously proposed by Dana Scott. Work on the LCF system introduced the general-purpose programming language ML to allow users to write theorem-proving tactics, supporting algebraic data types, parametric polymorphism, abstract data types, and exceptions.
- Hypernym
- Prover
- Is primary topic of
- Logic for Computable Functions
- Label
- enLogic for Computable Functions
- Link from a Wikipage to an external page
- www.dtic.mil/dtic/tr/fulltext/u2/785072.pdf
- www.cl.cam.ac.uk/~mjcg/papers/HolHistory.html
- Link from a Wikipage to another Wikipage
- Abstract data type
- Abstract data types
- Algebraic data type
- Automated theorem prover
- Category:Logic in computer science
- Category:Proof assistants
- Dana Scott
- Exception handling
- HOL (proof assistant)
- HOL Light
- Inference rule
- Isabelle proof assistant
- Logic of Computable Functions
- ML (programming language)
- Parametric polymorphism
- Programming language
- Robin Milner
- Stanford University
- Trusted computing base
- University of Edinburgh
- SameAs
- 4rDu4
- LCF
- Logic for Computable Functions
- Logic for Computable Functions
- Logic for Computable Functions
- m.015gtq
- Q6667462
- SeeAlso
- Logic of Computable Functions
- Subject
- Category:Logic in computer science
- Category:Proof assistants
- WasDerivedFrom
- Logic for Computable Functions?oldid=1107472529&ns=0
- WikiPageLength
- 5586
- Wikipage page ID
- 161900
- Wikipage revision ID
- 1107472529
- WikiPageUsesTemplate
- Template:Cite book
- Template:Cite manual
- Template:Mathlogic-stub
- Template:Refbegin
- Template:Refend
- Template:Reflist
- Template:See also
- Template:Short description