Logic and computation : interactive proof with Cambridge LCF
Lawrence Charles Paulson · Medical Entomology and Zoology · 1990
From the Publisher: This study of techniques for formal theorem-proving focuses on the applications of Cambridge LCF (Logic for Computable Functions), a computer program for reasoning about computation.