Strong Normalization for HA + EM1 by Non-Deterministic Choice
Logic in Computer Science
2013-09-06 v1
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 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".
Cite
@article{arxiv.1309.1254,
title = {Strong Normalization for HA + EM1 by Non-Deterministic Choice},
author = {Federico Aschieri},
journal= {arXiv preprint arXiv:1309.1254},
year = {2013}
}
Comments
In Proceedings COS 2013, arXiv:1309.0924