Getting results from programs extracted from classical proofs

DOI10.1016/J.TCS.2004.03.006MaRDI QIDQ1882897zbMATH OpenOpenAlexFDO

Authors Christophe Raffalli

Publication date 1 October 2004

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2004.03.006

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Refined program extraction from classical proofs
• Refined program extraction from classical proofs: Some case studies
• scientific article; zbMATH DE number 895269
• Extraction and verification of programs by analysis of formal proofs
• Practical program extraction from classical proofs

Cites work

• A general storage theorem for integers in call-by-name \(\lambda\)- calculus
• A semantics of evidence for classical arithmetic
• Dependent choice, `quote' and the clock
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 482822 (Why is no real title available?)
• Mixed logic and storage operators
• Pruning simply typed  -terms
• Refined program extraction from classical proofs
• The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction

Cited in

(12)

• The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction
• Extraction and verification of programs by analysis of formal proofs
• Programs from proofs using classical dependent choice
• Refined program extraction from classical proofs: Some case studies
• Practical program extraction from classical proofs
• Exploring the computational content of the infinite pigeonhole principle
• scientific article; zbMATH DE number 65537 (Why is no real title available?)
• scientific article; zbMATH DE number 1301852 (Why is no real title available?)
• Modal functional (``Dialectica) interpretation
• Refined program extraction from classical proofs
• PML2: integrated program verification in ML
• Program extraction from classical proofs

Describes a project that uses

Uses Software

• PhoX

This page was built for publication: Getting results from programs extracted from classical proofs

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