On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
Theor. Comput. Sci., Volume 625, 2016, Pages 125-146.
Abstract We present a new Curry–Howard correspondence for classical first-order natural deduction. We add to the lambda calculus an operator which represents, from the viewpoint of programming, a mechanism for raising and catching multiple exceptions, and from the viewpoint of logic, the excluded middle over arbitrary prenex formulas. T...More
Full Text (Upload PDF)
PPT (Upload PPT)