Extraction of redundancy-free programs from constructive natural deduction proofs

DOI10.1016/S0747-7171(08)80139-3MaRDI QIDQ808284zbMATH OpenFDO

Authors Yukihide Takayama

Publication date 1991

Published in Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

constructive logicprogram verificationautomated programmingproof treesrealizability interpretationredundancy-free codes

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Extraction and verification of programs by analysis of formal proofs
• scientific article; zbMATH DE number 895269
• Analysis of methods for extraction of programs from non-constructive proofs.
• Interactive realizers: a new approach to program extraction from nonconstructive proofs
• Writing constructive proofs yielding efficient extracted programs

Cites work

• scientific article; zbMATH DE number 3900744 (Why is no real title available?)
• scientific article; zbMATH DE number 3684934 (Why is no real title available?)
• scientific article; zbMATH DE number 3735770 (Why is no real title available?)
• scientific article; zbMATH DE number 3432235 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• The calculus of constructions

Cited in

(6)

• Extraction and verification of programs by analysis of formal proofs
• Writing constructive proofs yielding efficient extracted programs
• \(QPC_ 2\): A constructive calculus with parameterized specifications
• Defining concurrent processes constructively
• Extraction of a program from deduction and its regularity. I
• First order marked types

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication: Extraction of redundancy-free programs from constructive natural deduction proofs

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