Programs from proofs using classical dependent choice

DOI10.1016/J.APAL.2008.01.004zbMATH Open1136.03022OpenAlexW1982026859MaRDI QIDQ2482844FDOQ2482844

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

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

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)

Cites Work

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

Cited In (9)

• The equivalence of bar recursion and open recursion
• The Peirce translation
• Refined program extraction from classical proofs: Some case studies
• Title not available (Why is that?)
• Exploring the computational content of the infinite pigeonhole principle
• Refined program extraction from classical proofs
• A Constructive Proof of Dependent Choice, Compatible with Classical Logic
• Title not available (Why is that?)
• Dependent choice, `quote' and the clock

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)