Publication:4012886
From MaRDI portal
zbMath0754.03040MaRDI QIDQ4012886
Robert L. Constable, Chet Murthy
Publication date: 27 September 1992
constructive proofs; classical proofs; fragment of type theory; general method of extracting algorithms from classical proofs
03B35: Mechanization of proofs and logical operations
03F35: Second- and higher-order arithmetic and fragments
Related Items
A short proof of the strong normalization of classical natural deduction with disjunction, Refined program extraction from classical proofs, Uniform Heyting arithmetic, Programs from proofs using classical dependent choice
Uses Software