Writing programs that construct proofs

DOI10.1007/BF00244273zbMATH Open0615.68063OpenAlexW2019651724MaRDI QIDQ1820596FDOQ1820596

J. L. Bates, T. B. Knoblock, Robert Constable

Publication date: 1985

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00244273

Recommendations

• Proofs and programs
• Proving and programming
• scientific article; zbMATH DE number 4006266
• Foreword to the special focus on formal proofs for mathematics and computer science
• A Proof-Theoretic Approach to Tactics

zbMATH Keywords

LCFautomated reasoningdecision proceduresformal mathematicsproof checkingintelligent systemsAutomath

Mathematics Subject Classification ID

Cited In (12)

• Do-it-yourself type theory
• A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
• Formal proof of a program: find
• Programming as a mathematical exercise
• Title not available (Why is that?)
• Title not available (Why is that?)
• Innovations in computational type theory using Nuprl
• On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
• An intuitionistic theory of types with assumptions of high-arity variables
• An overview of the Tecton proof system
• Meta programming on the proof level
• Title not available (Why is that?)

Uses Software

• LCF

This page was built for publication: Writing programs that construct proofs

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