Search Results

Documents authored by Aschieri, Federico

Document
DOI: 10.4230/LIPIcs.TYPES.2016.4
On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic

Authors: Federico Aschieri and Matteo Manighetti

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)

Abstract
Intuitionistic first-order logic extended with a restricted form of Markov's principle is constructive and admits a Curry-Howard correspondence, as shown by Herbelin. We provide a simpler proof of that result and then we study intuitionistic first-order logic extended with unrestricted Markov's principle. Starting from classical natural deduction, we restrict the excluded middle and we obtain a natural deduction system and a parallel Curry-Howard isomorphism for the logic. We show that proof terms for existentially quantified formulas reduce to a list of individual terms representing all possible witnesses. As corollary, we derive that the logic is Herbrand constructive: whenever it proves any existential formula, it proves also an Herbrand disjunction for the formula. Finally, using the techniques just introduced, we also provide a new computational interpretation of Arithmetic with Markov's principle.
Cite as

Federico Aschieri and Matteo Manighetti. On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{aschieri_et_al:LIPIcs.TYPES.2016.4,
  author =	{Aschieri, Federico and Manighetti, Matteo},
  title =	{{On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{4:1--4:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.4},
  URN =		{urn:nbn:de:0030-drops-98590},
  doi =		{10.4230/LIPIcs.TYPES.2016.4},
  annote =	{Keywords: Markov's Principle, first-order logic, natural deduction, Curry-Howard}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2013.24
A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle

Authors: Federico Aschieri and Margherita Zorzi

Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

Abstract
We propose a very simple modification of Kreisel's modified realizability in order to computationally realize Markov's Principle in the context of Heyting Arithmetic. Intuitively, realizers correspond to arbitrary strategies in Hintikka-Tarski games, while in Kreisel's realizability they can only represent winning strategies. Our definition, however, does not employ directly game semantical concepts and remains in the style of functional interpretations. As term calculus, we employ a purely functional language, which is Goedel's System T enriched with some syntactic sugar.
Cite as

Federico Aschieri and Margherita Zorzi. A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 24-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{aschieri_et_al:LIPIcs.TYPES.2013.24,
  author =	{Aschieri, Federico and Zorzi, Margherita},
  title =	{{A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{24--44},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.24},
  URN =		{urn:nbn:de:0030-drops-46245},
  doi =		{10.4230/LIPIcs.TYPES.2013.24},
  annote =	{Keywords: Markov's Principle, Intuitionistic Realizability, Heyting Arithmetic, Game Semantics}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.45
Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1

Authors: Federico Aschieri, Stefano Berardi, and Giovanni Birolo

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

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

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)

Copy BibTex To Clipboard

@InProceedings{aschieri_et_al:LIPIcs.CSL.2013.45,
  author =	{Aschieri, Federico and Berardi, Stefano and Birolo, Giovanni},
  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 =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.45},
  URN =		{urn:nbn:de:0030-drops-41894},
  doi =		{10.4230/LIPIcs.CSL.2013.45},
  annote =	{Keywords: Interactive realizability, classical Arithmetic, witness extraction, delimited exceptions}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.31
Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms

Authors: Federico Aschieri

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
Interactive realizability is a computational semantics of classical Arithmetic. It is based on interactive learning and was originally designed to interpret excluded middle and Skolem axioms for simple existential formulas. A realizer represents a proof/construction depending on some state, which is an approximation of some Skolem functions. The realizer interacts with the environment, which may provide a counter-proof, a counterexample invalidating the current construction of the realizer. But the realizer is always able to turn such a negative outcome into a positive information, which consists in some new piece of knowledge learned about the mentioned Skolem functions. The aim of this work is to extend Interactive realizability to a system which includes classical first-order Peano Arithmetic with Skolem axioms. For witness extraction, the learning capabilities of realizers will be exploited according to the paradigm of learning by levels. In particular, realizers of atomic formulas will be update procedures in the sense of Avigad and thus will be understood as stratified-learning algorithms.
Cite as

Federico Aschieri. Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 31-45, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{aschieri:LIPIcs.CSL.2012.31,
  author =	{Aschieri, Federico},
  title =	{{Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{31--45},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.31},
  URN =		{urn:nbn:de:0030-drops-36629},
  doi =		{10.4230/LIPIcs.CSL.2012.31},
  annote =	{Keywords: Interactive realizability, learning, classical Arithmetic, witness extraction}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.20
Transfinite Update Procedures for Predicative Systems of Analysis

Authors: Federico Aschieri

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
We present a simple-to-state, abstract computational problem, whose solution implies the 1-consistency of various systems of predicative Analysis and offers a way of extracting witnesses from classical proofs. In order to state the problem, we formulate the concept of transfinite update procedure, which extends Avigad's notion of update procedure to the transfinite and can be seen as an axiomatization of learning as it implicitly appears in various computational interpretations of predicative Analysis. We give iterative and bar recursive solutions to the problem.
Cite as

Federico Aschieri. Transfinite Update Procedures for Predicative Systems of Analysis. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 20-34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{aschieri:LIPIcs.CSL.2011.20,
  author =	{Aschieri, Federico},
  title =	{{Transfinite Update Procedures for Predicative Systems of Analysis}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{20--34},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.20},
  URN =		{urn:nbn:de:0030-drops-32200},
  doi =		{10.4230/LIPIcs.CSL.2011.20},
  annote =	{Keywords: update procedure, epsilon substitution method, predicative classical analysis, bar recursion}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact