scientific article; zbMATH DE number 3684934

MaRDI QIDQ3880322zbMATH OpenFDO

Authors C. A. Goad

Publication date 1980

zbMATH Keywords

automatic transformation of algorithmsdescriptions of computationmanipulating proofsproof theory

Mathematics Subject Classification ID

Proof theory and constructive mathematics (03F99) Software, source code, etc. for problems pertaining to computer science (68-04) Abstract data types; algebraic specification (68Q65) Algorithms in computer science (68W99)

Cited in

(11)

• Extracting Lisp programs from constructive proofs: A formal theory of constructive mathematics based on Lisp
• Programs as proofs: A synopsis
• A proof description language and its reduction system
• History and basic features of the critical-pair/completion procedure
• Proof normalization with nonstandard objects
• \(QPC_ 2\): A constructive calculus with parameterized specifications
• Some remarks on the possibility of extending resolution proof procedures to intuitionistic logic
• Extraction and verification of programs by analysis of formal proofs
• Semantics of algorithmic languages
• Extraction of redundancy-free programs from constructive natural deduction proofs
• Constructive system for automatic program synthesis

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3880322)