Programs as proofs: A synopsis

DOI10.1016/0020-0190(83)90060-1zbMath0514.68043OpenAlexW2031973846MaRDI QIDQ1051424

Robert L. Constable

Publication date: 1983

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0020-0190(83)90060-1

zbMATH Keywords

constructive proofprogram

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Algorithms in computer science (68W99)

Related Items (5)

Automatic synthesis of typed \(\Lambda\)-programs on term algebras ⋮ Implementing Euclid's straightedge and compass constructions in type theory ⋮ Synthesis of list algorithms by mechanical proving ⋮ Some remarks on the possibility of extending resolution proof procedures to intuitionistic logic ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction

Uses Software

• ALGOL 68
• Automath
• LCF

Cites Work

• An introduction to the PL/CV2 programming logic
• Edinburgh LCF. A mechanized logic of computation
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Programming as a Discipline of Mathematical Nature
• An axiomatic basis for computer programming
• On the interpretation of intuitionistic number theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Programs as proofs: A synopsis