Extracting Lisp programs from constructive proofs: A formal theory of constructive mathematics based on Lisp

DOI10.2977/prims/1195182982zbMath0513.68022OpenAlexW1987110844MaRDI QIDQ1050769

Susumu Hayashi

Publication date: 1983

Published in: Publications of the Research Institute for Mathematical Sciences, Kyoto University (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2977/prims/1195182982

zbMATH Keywords

automatic program synthesisconstructive formal proofsformal verificationsq-realizability

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01) Proof theory and constructive mathematics (03F99)

Related Items

Towards a computation system based on set theory

Cites Work

• Theory of symbolic expressions. I
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
• Toward automatic program synthesis
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item