Strong Normalization for HA + EM1 by Non-Deterministic Choice

COS, pp. 1-14, 2013.

Cited by: 3|Bibtex|Views0|Links
EI

Abstract:

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

Code:

Data:

Your rating :
0

 

Tags
Comments