Now showing items 1-4 of 4

    • Classical Proofs as Programs: How, What and Why 

      Murthy, Chetan R. (Cornell University, 1991-07)
      We recapitulate Friedman's conservative extension result of(suitable) classical over constructive systems for $\Pi_{2}^{0}$sentences, viewing it in two lights: as a translation of programs from an almost-functional ...
    • A Constructive Proof of Higman's Lemma 

      Murthy, Chetan R.; Russell, James R. (Cornell University, 1989-10)
      Higman's Lemma is a special case of the more general Kruskal's tree embedding theorem and the graph minor theorem. Prior to this work, only classical (and impredicative) proofs of the Lemma were known. Recently, there ...
    • An Evaluation Semantics for Classical Proofs 

      Murthy, Chetan R. (Cornell University, 1991-06)
      We show how to interpret classical proofs as programs in a way that agrees with the well-known treatment of constructive proofs as programs and moreover extends it to give a computational meaning to proofs claiming the ...
    • Extracting Constructive Content from Classical Proofs 

      Murthy, Chetan R. (Cornell University, 1990-08)
      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 ...