scientific article
From MaRDI portal
Publication:4012886
zbMath0754.03040MaRDI QIDQ4012886
Chet Murthy, Robert L. Constable
Publication date: 27 September 1992
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
constructive proofsclassical proofsfragment of type theorygeneral method of extracting algorithms from classical proofs
Mechanization of proofs and logical operations (03B35) Second- and higher-order arithmetic and fragments (03F35)
Related Items
A short proof of the strong normalization of classical natural deduction with disjunction ⋮ Programs from proofs using classical dependent choice ⋮ Uniform Heyting arithmetic ⋮ Refined program extraction from classical proofs ⋮ Programs with continuations and linear logic ⋮ On preserving the computational content of mathematical proofs: toy examples for a formalising strategy
Uses Software