Proofs as programs

DOI10.1145/2363.2528zbMath0555.68003OpenAlexW2021790140MaRDI QIDQ3219093

J. L. Bates, Robert L. 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 specificationintelligent systemsprogram correctnessprogram refinementautomatic programmingautomated logiccostructive logicvery high level programming languages

Mathematics Subject Classification ID

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

Related Items (13)

The effects of effects on constructivism ⋮ Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study ⋮ Generalization from partial parametrization in higher-order type theory ⋮ Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language ⋮ Expressing computational complexity in constructive type theory ⋮ Synthesis of list algorithms by mechanical proving ⋮ A higher-order interpretation of deductive tableau ⋮ Unnamed Item ⋮ Presenting intuitive deductions via symmetric simplification ⋮ HasCasl: integrated higher-order specification and program development ⋮ A note on complexity measures for inductive classes in constructive type theory ⋮ Automated higher-order complexity analysis ⋮ Enumerating \(k\)-way trees

This page was built for publication: Proofs as programs