lcf theorem prover

An interactive theorem prover developed at the universities of Edinburgh and Stanford by Robin Milner and others. LCF introduced the general purpose programming language ML to allow users to write theorem proving tactics. Theorems in the system are propositions of a special "theorem" abstract datatype. The ML type system ensures that theorems are derived using only the inference rules given by the operations of the abstract type. Successors include the HOL and Isabelle theorem provers.

<< Previous

Word Browser

Next >>

louis ii of france
katie hnida
chain
days of wine and roses
marcello mastroianni
divorce, italian style
dana scott
this sporting life
clean programming language
scalar field
hud (movie)

uniqueness type
cat ballou
formal methods
the spy who came in from the cold
isabelle theorem prover
the pawnbroker
hol theorem prover
douglas dunn
oskar werner
carl czerny
alan arkin

herb ritts
cool hand luke
cliff robertson
edge of sanity
charly
the heart is a lonely hunter
computer program analysis
alan bates
the fixer
ron moody
emigration

true grit
melvyn douglas
i never sang for my father
the great white hope
gulbuddin hekmatyar
jacopo peri
ryan o'neal
predicative verb
sunday bloody sunday
glottal consonant
kotch