Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1

Aschieri, Federico; Berardi, Stefano; Birolo, Giovanni

doi:10.4230/LIPIcs.CSL.2013.45

Document

Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1

Authors Federico Aschieri, Stefano Berardi, Giovanni Birolo

Part of: Volume: Computer Science Logic 2013 (CSL 2013)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: Computer Science Logic (CSL)
License: Creative Commons Attribution 3.0 Unported license
Publication Date: 2013-09-02

PDF

File

PDF

LIPIcs.CSL.2013.45.pdf

Filesize: 0.6 MB
16 pages

Document Identifiers

DOI: 10.4230/LIPIcs.CSL.2013.45
URN: urn:nbn:de:0030-drops-41894

Subject Classification

Keywords

Interactive realizability
classical Arithmetic
witness extraction
delimited exceptions

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

Abstract

We present a new Curry-Howard correspondence for HA + EM_1, constructive Heyting Arithmetic with the excluded middle on \Sigma^0_1-formulas. We add to the lambda calculus 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 motivate the restriction of the excluded middle by its use in proof mining; we introduce new techniques to prove strong normalization for HA + EM_1 and the witness property for simply existential statements. One may consider our results as an application of the ideas of Interactive realizability, which we have adapted to the new setting and used to prove our main theorems.

Cite As Get BibTex

Federico Aschieri, Stefano Berardi, and Giovanni Birolo. Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 45-60, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013) https://doi.org/10.4230/LIPIcs.CSL.2013.45

Author Details

Federico Aschieri

Stefano Berardi

Giovanni Birolo

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail