Classical Proofs as Programs

摘要: We present an extension of the correspondence between intuitionistic proofs and functional programs to classical proofs, more precisely second order proofs. The advantage logic in this context is that it allows model imperative features programming languages too (cf [5]). But there intrinsic difficulty with which lies certain non-determinism its computational interpretations. use a natural deduction system removes part non determinism by fixing inputs left sequents [10] [11]). However conflict remains confluence computation mechanism uniqueness representation data (for instance number 1). In paper we develop solution problem proposed [11]: show how extract from one using “output” operator, while keeping confluent mechanism. This result extend sound way proofs-as-programs paradigm framework where all usual theoretical properties still hold.