Extraction of redundancy-free programs from constructive natural deduction proofs

DOI10.1016/S0747-7171(08)80139-3zbMATH Open0731.68079MaRDI QIDQ808284FDOQ808284

Authors: Yukihide Takayama 

Publication date: 1991

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

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

zbMATH Keywords

constructive logicprogram verificationautomated programmingproof treesrealizability interpretationredundancy-free codes

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The calculus of constructions
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (6)

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

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)