Extracting Constructive Content from Classical Proofs

Other Titles


This thesis is concerned with the relationship between classical and constructive mathematics. It is well-known that in many constructive logics, we can interpret mathematical sentences as program specifications, and we can interpret a constructive proof of such a sentence as a program which meets this specification. It is also well-known that many classical logics do not have the property, as shown by Brouwer's counterexamples to some theorems of analysis. Kreisel and Friedman showed that for certain classes of sentences (Π20), the classical theories conservatively extend their constructive counterparts, and furthermore give effective translations from classical proofs to constructive proofs. This thesis consists of two parts. In the first, we describe our implementation of Friedman's translation results, and their use in translating Higman's Lemma, a nontrivial theorem of combinatorics. To do this, we delineate a subtheory of a constructive type theory (Nuprl) for which Friedman's translation is guaranteed to succeed. We also extend the Nuprl type theory with impredicative Π-quantification, and use this to provide a classical proof of Higman's Lemma, which we go on to mechanically translate to a constructive proof. In the second part, we discuss connections that we have discovered between Friedman's translation and a standard compilation technique, continuation-passing-style (CPS) translation. We demonstrate that a classical proof of a (Π20) sentence Φ is a program which meets the specification Φ. We demonstrate that we can consistently give algorithmic content to the only constructively problematic rule of classical logic, the rule of double-negation elimination. This algorithmic content is the nonlocal control operator C (a relative of call-with-current-continuation). Moreover, we show that Friedman's translation is exactly a CPS-translation on the classical "program" (with C), converting it into a pure functional program (without C). Our work provides a semantic account of Friedman's translation, in terms of its effect on programs, making the connections (and the differences) between classical and constructive systems clearer and more precise. Moreover, we provide the first steps towards integrating nonlocal control operators into a type-theoretic explanation of computation.

Journal / Series

Volume & Issue



Date Issued



Cornell University


computer science; technical report


Effective Date

Expiration Date




Union Local


Number of Workers

Committee Chair

Committee Co-Chair

Committee Member

Degree Discipline

Degree Name

Degree Level

Related Version

Related DOI

Related To

Related Part

Based on Related Item

Has Other Format(s)

Part of Related Item

Related To

Related Publication(s)

Link(s) to Related Publication(s)


Link(s) to Reference(s)

Previously Published As

Government Document




Other Identifiers


Rights URI


technical report

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record