LCF es un demostrador automático de teoremas interactivo desarrollado en la Universidad de Edimburgo y la Universidad de Stanford por Robin Milner y otros.
[1] LCF introdujo el lenguaje de programación ML, para permitir al usuario escribir tácticas de demostración.
Los teoremas en LCF son proposiciones del tipo de dato abstracto teorema.
[2] El sistema de tipos de ML garantiza que solo proposiciones demostradas basadas en axiomas y reglas de inferencia tengan el tipo teorema.
Entre los lenguajes de programación descendientes de ML están Standard ML y OCaml.