Strong Normalization for HA + EM1 by Non-Deterministic Choice
Federico Aschieri (ENS de Lyon, Universit\'e de Lyon)
TL;DR
This paper proves strong normalization for a logical system combining Heyting Arithmetic with a restricted excluded middle, using a novel non-deterministic immersion technique in the proof calculus.
Contribution
It introduces a new proof of strong normalization for HA + EM1 leveraging non-deterministic immersion, connecting programming exceptions with logical principles.
Findings
Strong normalization established for HA + EM1
Non-deterministic immersion technique developed
Logical-exception operator correspondence demonstrated
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".
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.