Writing constructive proofs yielding efficient extracted programs

MaRDI QIDQ2703717zbMATH OpenFDO

Authors Aleksey Nogin

Publication date 7 May 2001

zbMATH Keywords

Myhill-Nerode automata minimization theoremNuprl automata library

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Formal languages and automata (68Q45)

Recommendations

• Extraction and verification of programs by analysis of formal proofs
• scientific article; zbMATH DE number 177798
• Extraction of redundancy-free programs from constructive natural deduction proofs
• Proofs and programs: A naïve approach to program extraction
• Analysis of methods for extraction of programs from non-constructive proofs.

Cited in

(6)

• The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction
• Proof pearl: constructive extraction of cycle finding algorithms
• scientific article; zbMATH DE number 2185653 (Why is no real title available?)
• Extracting Algorithms from Intuitionistic Proofs
• scientific article; zbMATH DE number 2090125 (Why is no real title available?)
• Extraction of redundancy-free programs from constructive natural deduction proofs

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication: Writing constructive proofs yielding efficient extracted programs

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