Electronic Proceedings in Theoretical Computer Science (Sep 2013)

Strong Normalization for HA + EM1 by Non-Deterministic Choice

  • Federico Aschieri

DOI
https://doi.org/10.4204/EPTCS.127.1
Journal volume & issue
Vol. 127, no. Proc. COS 2013
pp. 1 – 14

Abstract

Read online

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 delimited scope, and from the viewpoint of logic, a restricted version of the excluded middle. We give a strong normalization proof for the system based on a technique of "non-deterministic immersion".