LARA

Higher-Order Logic and Interactive Provers

Lambda Calculus

Untyped Lambda Calculus

Simply Typed Lambda Calculus

Further reading:

Classical Higher-Order Logic (HOL)

Syntax and Shorthands of HOL

Standard-Model Semantics of HOL

Axioms of HOL

Results Proved in HOL

Further reading:

LCF Theorem Proving Approach

Approaches to Reliable Complex Proofs

Immutable Abstract Data Types

Theorems as Abstract Data Types

Proof and Code Generation in LCF Systems

Binary Search Trees Example

Further reading:

  • A Metalanguage for interactive proof in LCF - ML stands for meta-Language, because it was a language for writing theorem provers that prove theorems (in object-language i.e. logic of computable functions)
  • Upcoming book “Introduction to Logic and Automated Theorem Proving” by John Harrison
  • Logic and Computation: Interactive Proof with Cambridge LCF

Some Interactive Provers

HOL - use directly ML

HOL Light - compact version, written in OCaml

Isabelle - popular, ML part largely hidden

PVS - automation through decision procedures

Coq - was less automated, now catching up; more complex logic

NuPRL - more complex type theory, constructive mathematics

ACL2 - emphasis on executable functions, quantifier-free statements, automated induction, pioneering industrial-scale case studies

Example Results in Isabelle

NipkowETAL06FlyspeckI,
Paulson03ConsistencyAxiomChoiceIsabelle,
PaulsonGrabczewski96MechanizingSetTheory,
Berghofer07FirstOrderLogicAccordingtoFitting