Programs from proofs using classical dependent choice

DOI10.1016/J.APAL.2008.01.004MaRDI QIDQ2482844zbMATHOpenAlexFDO

Authors Monika Seisenberger

Publication date 24 April 2008

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2008.01.004

zbMATH Keywords

\(A\)-translationclassical dependent choicecomputational content of classical proofsinfinite tape exampleMinlog

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Metamathematics of constructive systems (03F50) Functionals in proof theory (03F10)

Recommendations

• scientific article; zbMATH DE number 895269
• Refined program extraction from classical proofs
• Refined program extraction from classical proofs: Some case studies
• scientific article; zbMATH DE number 2247255
• Refinement of classical proofs for program extraction

Cites work

• scientific article; zbMATH DE number 4033746 (Why is no real title available?)
• scientific article; zbMATH DE number 65537 (Why is no real title available?)
• scientific article; zbMATH DE number 3614784 (Why is no real title available?)
• scientific article; zbMATH DE number 1301733 (Why is no real title available?)
• scientific article; zbMATH DE number 1552509 (Why is no real title available?)
• scientific article; zbMATH DE number 2174396 (Why is no real title available?)
• scientific article; zbMATH DE number 2085177 (Why is no real title available?)
• scientific article; zbMATH DE number 2222013 (Why is no real title available?)
• scientific article; zbMATH DE number 2247255 (Why is no real title available?)
• scientific article; zbMATH DE number 3198033 (Why is no real title available?)
• A general storage theorem for integers in call-by-name \(\lambda\)- calculus
• A syntactic theory of sequential control
• Constructive topology and combinatorics
• Dependent choice, `quote' and the clock
• Ein starker Normalisationssatz für die bar-rekursiven Funktionale
• Getting results from programs extracted from classical proofs
• On the computational content of the axiom of choice
• Proving open properties by induction
• Recursive programming with proofs
• Refined program extraction from classical proofs
• The greatest common divisor: A case study for program extraction from classical proofs
• Theorem Proving in Higher Order Logics
• Types for Proofs and Programs
• Uniform Heyting arithmetic
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(10)

• A Constructive Proof of Dependent Choice, Compatible with Classical Logic
• scientific article; zbMATH DE number 2247255 (Why is no real title available?)
• Dependent choice, `quote' and the clock
• The equivalence of bar recursion and open recursion
• scientific article; zbMATH DE number 2185652 (Why is no real title available?)
• The Peirce translation
• Refined program extraction from classical proofs
• Refined program extraction from classical proofs: Some case studies
• Exploring the computational content of the infinite pigeonhole principle
• Refinement of classical proofs for program extraction

Describes a project that uses

Uses Software

• ACL2

This page was built for publication: Programs from proofs using classical dependent choice

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