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.

Cited by: 22|Bibtex|Views14|Links
EI

Abstract:

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

Code:

Data:

Your rating :
0

 

Tags
Comments