## Paper: An evaluation semantics for classical proofs (at LICS 1991)

**Chetan R. Murthy**

### Abstract

It is shown 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 existence of a value satisfying
a recursive predicate. The method turns out to be equivalent to H. Friedman's (Lecture Notes in Mathematics, vol.699, p.21-28,
1978) proof by A -transition of the conservative extension of classical cover constructive arithmetic for II_{2}^{0} sentences. It is shown that Friedman's result is a proof-theoretic version of a semantics-preserving CPS-translation from
a nonfunctional programming language back to a functional programming language. A sound evaluation semantics for proofs in
classical number theory (PA) of such sentences is presented as a modification of the standard semantics for proofs in constructive
number theory (HA). The results soundly extend the proofs-as-programs paradigm to classical logics and to programs with the
control operator, C

### BibTeX

@InProceedings{Murthy-Anevaluationsemanti, author = {Chetan R. Murthy}, title = {An evaluation semantics for classical proofs}, booktitle = {Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991)}, year = {1991}, month = {July}, pages = {96--107}, location = {Amsterdam, The Netherlands}, publisher = {IEEE Computer Society Press} }