License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2013.45
URN: urn:nbn:de:0030-drops-41894
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4189/
Go to the corresponding LIPIcs Volume Portal

Aschieri, Federico ; Berardi, Stefano ; Birolo, Giovanni

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

pdf-format:
9.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{aschieri_et_al:LIPIcs:2013:4189,
  author =	{Federico Aschieri and Stefano Berardi and Giovanni Birolo},
  title =	{{Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{45--60},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Simona Ronchi Della Rocca},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4189},
  URN =		{urn:nbn:de:0030-drops-41894},
  doi =		{10.4230/LIPIcs.CSL.2013.45},
  annote =	{Keywords: Interactive realizability, classical Arithmetic, witness extraction, delimited exceptions}
}

Keywords: Interactive realizability, classical Arithmetic, witness extraction, delimited exceptions
Collection: Computer Science Logic 2013 (CSL 2013)
Issue Date: 2013
Date of publication: 02.09.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI