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

automated logicautomatic programmingcostructive logicintelligent systemsprogram correctnessprogram refinementprogram specificationvery high level programming languages

Mathematics Subject Classification ID

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

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)

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

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)