The Peirce Translation and the Double Negation Shift
computational extraction of witnesses from proofs in classical analysis
scientific article