Lessons learned from LCF: A Survey of Natural Deduction Proofs

DOI10.1093/COMJNL/28.5.474MaRDI QIDQ3696549zbMATH OpenOpenAlexFDO

Authors Lawrence C. Paulson

Publication date 1985

Published in The Computer Journal (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/comjnl/28.5.474

zbMATH Keywords

interactive theorem provingverification of hardware and software

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verifying the unification algorithm in LCF
• Natural deduction as higher-order resolution
• A few exercises in theorem processing
• scientific article; zbMATH DE number 3880145
• From LCF to Isabelle/HOL

Cited in

(5)

• Verifying the unification algorithm in LCF
• Constructing recursion operators in intuitionistic type theory
• Terminating general recursion
• Implementing theorem provers in a purely functional style
• A few exercises in theorem processing

This page was built for publication: Lessons learned from LCF: A Survey of Natural Deduction Proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3696549)