Proofs as programs

DOI10.1145/2363.2528zbMATH Open0555.68003OpenAlexW2021790140MaRDI QIDQ3219093FDOQ3219093

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/

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

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)

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
• Expressing computational complexity in constructive type theory
• Proofs-as-programs as a framework for the design of an analogy-based ML editor
• Formal proof of a program: find
• What Is the Difference Between Proofs and Programs?
• Title not available (Why is that?)
• Automated higher-order complexity analysis
• A note on complexity measures for inductive classes in constructive type theory
• A machine program for theorem-proving
• Generalization from partial parametrization in higher-order type theory
• The effects of effects on constructivism
• Proofs and programs
• Presenting intuitive deductions via symmetric simplification
• Enumerating \(k\)-way trees
• Proof methods of declarative properties of definite programs
• 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)