Classical Proofs as Parallel Programs
GandALF, pp. 43-57, 2018.
We introduce a first proofs-as-parallel-programs correspondence for classical logic. We define a parallel and more powerful extension of the simply typed lambda calculus corresponding to an analytic natural deduction based on the excluded middle law. The resulting functional language features a natural higher-order communication mechanism...More
Full Text (Upload PDF)
PPT (Upload PPT)