LCF

LCF és un demostrador automàtic de teoremes interactiu desenrollat en l'Universitat d'Edimburc i l'Universitat de Stanford per Robin Milner i uns atres.

LCF va introduir el llenguage de programació ML, per a permetre a l'usuari escriure tàctiques de demostració. Les teoremes en LCF són proposicions del tipo de senya abstracta teorema. El sistema de tipos de ML garantisa que solament proposicions demostrades basades en axioma i regles d'inferència tinguen el tipo teorema.

Entre els successors de LCF estan els demostradores de teoremes HOL i Isabelle. Entre els llenguages de programació descendents de ML estan Standard ML i OCaml.