Skip to main content

Use this tag for proof assistants that are generic, in that they allow a variety of logics to used with them

Logical frameworks provide a uniform way of encoding a logical language, its inference rules and its proofs.

Use this tag for proof assistants that are generic, in that they allow a variety of logics to used with them.

Web pages:

Logical Frameworks by Frank Pfenning
Specific Logical Frameworks and Implementations by Frank Pfenning

Papers:

"From LCF to HOL: a short history" by Mike Gordon (pdf)