Strong Normalization for HA + EM1 by Non-Deterministic Choice
COS, pp. 1-14, 2013.
We study the strong normalization of a new Curry-Howard correspondence for HA + EM1, constructive Heyting Arithmetic with the excluded middle on Sigma01-formulas. The proof-term language of HA + EM1 consists in the lambda calculus plus an operator ||_a which represents, from the viewpoint of programming, an exception operator with a del...More
PPT (Upload PPT)