Proofs as programs

DOI10.1145/2363.2528MaRDI QIDQ3219093zbMATH OpenOpenAlexFDO

Authors J. L. Bates, Robert Constable

Publication date 1985

Published in ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL http://www.acm.org/pubs/contents/journals/toplas/1985-7/

zbMATH Keywords

program specificationprogram correctnessprogram refinementautomatic programmingintelligent systemsautomated logiccostructive logicvery high level programming languages

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Abstract data types; algebraic specification (68Q65)

Recommendations

• scientific article; zbMATH DE number 4006266
• Proofs and programs: A naïve approach to program extraction
• Some proofs of data refinement
• scientific article; zbMATH DE number 4147469
• A calculus of refinements for program derivations

Cited in

(21)

• Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study
• Intuitionistic ancestral logic as a dependently typed abstract programming language
• Proofs-as-programs as a framework for the design of an analogy-based ML editor
• Expressing computational complexity in constructive type theory
• Formal proof of a program: find
• Automated higher-order complexity analysis
• What Is the Difference Between Proofs and Programs?
• scientific article; zbMATH DE number 7552282 (Why is no real title available?)
• A note on complexity measures for inductive classes in constructive type theory
• Generalization from partial parametrization in higher-order type theory
• A machine program for theorem-proving
• The effects of effects on constructivism
• Proofs and programs
• Enumerating k-way trees
• Proof methods of declarative properties of definite programs
• Presenting intuitive deductions via symmetric simplification
• Proofs as processes
• Synthesis of list algorithms by mechanical proving
• HasCasl: integrated higher-order specification and program development
• From programming-by-example to proving-by-example
• A higher-order interpretation of deductive tableau

This page was built for publication: Proofs as programs

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