Proofs as programs
From MaRDI portal
Publication:3219093
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/
program specificationintelligent systemsprogram correctnessprogram refinementautomatic programmingautomated logiccostructive logicvery high level programming languages
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
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 ⋮ 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
