ÿþ<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"> <!-- saved from url=(0032) --> <!-- Begin included header --><HTML><HEAD><TITLE>Federico Aschieri's Page - PPS/INRIA</TITLE> <META http-equiv=Content-Type content="text/html; charset=iso-8859-1"> <META content="MSHTML 6.00.2900.2963" name=GENERATOR> <script type="text/javascript"> function showhide(spoiler) { gp = spoiler.parentNode.parentNode; if ( gp.getElementsByTagName( 'div' )[1].getElementsByTagName( 'div' )[0].style.display != '') { gp.getElementsByTagName( 'div' )[1].getElementsByTagName( 'div' )[0].style.display = ''; spoiler.value = 'Hide'; } else { gp.getElementsByTagName( 'div' )[1].getElementsByTagName( 'div' )[0].style.display = 'none'; spoiler.value = 'Abstract'; } } </script> </HEAD> <BODY text=#000000 vLink=#800000 link=#cc3300 bgColor=#eeeeee background=index_file/sandston.gif> <CENTER> <TABLE width="90%"> <TBODY> <TR> <TD colSpan=2> <HR noShade> </TD></TR> <TR> <TD noWrap align=middle><FONT color=black><B><FONT size=+2>L</FONT>ABORATOIRE <FONT size=+2>PPS</FONT> ||| <FONT size=+2>E</FONT>QUIPE <FONT size=+2>INRIA</FONT> &pi;&thinsp;r<sup>2</sup> &nbsp; <BR>Université Paris 7 </B></FONT></TD></TR> <TR> <TD colSpan=2> <HR noShade> </TD></TR> <TR> </TR> </TBODY> </TABLE> <TABLE width="90%"> <TBODY> <TR> <TD><!-- End included header --> <CENTER><IMG height=70 alt="THE GROUP'S LOGO" src="pps.gif" border=1> <BR><B>Research on "Preuves, Programmes et Systèmes"</B> </CENTER> <HR> <TABLE border=7> <TBODY></TBODY></TABLE> <TABLE> <TBODY> <TR> <TD><A href="foto.jpg"><IMG src="foto.jpg" align=middle border=2 with = 440 height = 220> </A></TD> <TD> <H1>Federico Aschieri, PhD</H1><A href="http://www.pps.jussieu.fr/">Laboratoire Preuves, Programmes et Systèmes</A><BR><a href="http://www.pps.jussieu.fr/pi.r2/">Equipe Inria &pi;&thinsp;<i>r</i><sup><i>2</i></sup></a> <BR><A href="http://www.univ-paris-diderot.fr/">Université Paris Diderot - Paris 7 </A><BR><B>Office:</B> Room 32, 5th floor <BR><B>Adress:</B> INRIA, 23 Avenue d'Italie, 75214 Paris<BR><B>Tel.</B> +33 0139635924 <BR><B>E-mail:</B> aschieri[AT]di.unito.it </TD></TR> </TBODY> </TABLE> </TABLE> <BR> <hr style="width: 100%; height: 2px;"> <div style="text-align: left;"> <p><b>ABOUT ME:</b> </p> I have done my PhD studies at Universita' degli Studi di Torino and <A href="http://www.dcs.qmul.ac.uk">Queen Mary, University of London</A>, from January 2008 to December 2010. From 3rd october 2011 I am postdoc at INRIA. Here is my <a href="Curriculum.pdf">Curriculum Vitae</a> </div> <hr style="width: 100%; height: 2px;"> <div style="text-align: left;"> <p><b>RESEARCH:</b> </p> <ul> <li><b>Interests</b>: Lambda Calculus, Type Systems, Proof Theory, Intuitionistic and Classical Logic, Computational Complexity and Combinatorics</li></div> <hr style="width: 100%; height: 2px;"> <div style="text-align: left;"> <p><b>PHD THESIS:</b> </p> <ul> <li> <i>Learning, Realizability and Games in Classical Arithmetic</i><br>Final Version, April 2011<br>(<a href="http://arxiv.org/abs/1012.4992 ">pdf</a>)</li></div> <hr style="width: 100%; height: 2px;"> <div style="text-align: left;"> <p><b>ARTICLES:</b> </p> <ul> <li> Aschieri, <a href="http://www-lipn.univ-paris13.fr/~zorzi/">Zorzi</a><br> <i>Eliminating Skolem Functions in Peano Arithmetic with Interactive Realizability</i> <br>Submitted <br> <div class="quotetitle"> <input type="button" value="Abstract" onclick="showhide(this);" ></div> <div class="quotecontent"><div style="display: none;">We present a new syntactical proof that first-order Peano Arithmetic with Skolem axioms is conservative over Peano Arithmetic alone for arithmetical formulas. This result -- which shows that the Excluded Middle principle can be used to eliminate Skolem functions -- has been previously proved by other techniques, among them the epsilon substitution method and forcing. In this paper, we employ Interactive Realizability, a computational semantics for Peano Arithmetic which extends Kreisel's modified realizability to the classical case. </div></div> <br><br> <li> Aschieri<br> <i>Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms</i> <br>Submitted <br> <div class="quotetitle"> <input type="button" value="Abstract" onclick="showhide(this);" ></div> <div class="quotecontent"><div style="display: none;">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. </div></div> <br><br> <li> Aschieri<br> <i>Interactive Realizability for Second-Order Heyting Arithmetic with EM1 and SK1</i> <br>Submitted <br> <div class="quotetitle"> <input type="button" value="Abstract" onclick="showhide(this);" ></div> <div class="quotecontent"><div style="display: none;">We introduce a classical realizability semantics based on interactive learning for full second-order Heyting Arithmetic with excluded middle and Skolem axioms over Sigma01-formulas. Realizers are written in a classical version of Girard's System F. Since the usual computability semantics does not apply to such a system, we introduce a constructive forcing/computability semantics: though realizers are not computable functional in the sense of Girard, they can be <i>forced</i> to be computable. We apply these semantics to show how to extract witnesses from realizable Pi02-formulas. In particular a constructive and efficient method is introduced. It is based on a new ''(state-extending-continuation)-passing-style translation'' whose properties are described with the constructive forcing/computability semantics.</div></div> (<a href="RealizabilityHASEM1final.pdf">pdf</a>) (<a href="http://hal.inria.fr/hal-00657054/fr/">HAL</a>) <br><br> <li> Aschieri, Berardi<br> <i>A New Use of Friedman's Translation: Interactive Realizability</i> <br>Festschrift of Helmut Schwichtenberg, Ontos-Verlag Series in Mathematical Logic, to appear <div class="quotetitle"> <input type="button" value="Abstract" onclick="showhide(this);" ></div> <div class="quotecontent"><div style="display: none;">Friedman's translation is a well-known transformation of formulas. The Friedman translation has two properties: i) it validates intuitionistic theorems -- if a formula is intuitionistically provable, then so it is its Friedman translation; ii) it is suitable for program extraction from classical proofs -- the intuitionistic provability of the Friedman translation of the negative translation of a for-all-exist-formula implies the intuitionistic provability of the formula itself. However, the Friedman translation does not validate classical principle, like the Excluded Middle.<br> Here, we define a restricted Friedman translation which both validates the Excluded Middle and Skolem axiom schemata restricted to $\Sigma^0_1$-formulas and it is also suitable for program extraction from classical proofs using such principles: the intuitionistic provability of the restricted Friedman translation of a for-all-exist-formula implies the intuitionistic provability of the formula itself. Then we introduce a learning-based Realizability Semantics for Heyting Arithmetic with all finite types, extended with the two previous axiom schemata. We call this semantics "Interactive Realizability", and we characterize it as the composition of our Friedman translation with Kreisel modified realizability. As a corollary, we show that Interactive Realizability is, in a sense, "axiom-driven", while the other Realizability Semantics for Classical Arithmetic, like the semantics of Krivine, are "goal-driven". </div></div> (<a href="InteractiveRealizabilityFriedman.pdf">pdf</a>) <br><br> <li> Aschieri<br> <i>Transfinite Update Procedures for Predicative Systems of Analysis</i> <br>Proceedings of Computer Science Logic 2011 (CSL 2011), Leibniz International Proceedings in Computer Science, vol. 12, 2011 <br> <div class="quotetitle"> <input type="button" value="Abstract" onclick="showhide(this);" ></div> <div class="quotecontent"><div style="display: none;">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.</div></div> (<a href="UpdateProcedures.pdf">pdf</a>) <br><br> <li> Aschieri<br> <i>Learning Based Realizability for HA + EM1 and 1-Backtracking Games: Soundness and Completeness</i> <br>Annals of Pure and Applied Logic, accepted <div class="quotetitle"><input type="button" value="Abstract" onclick="showhide(this);" ></div> <div class="quotecontent"><div style="display: none;">We prove a soundness and completeness result for Aschieri and Berardi's learning based realizability for Heyting Arithmetic plus Excluded Middle over semi-decidable statements with respect to 1-Backtracking Coquand game semantics. First, we prove that learning based realizability is sound with respect to 1-Backtracking Coquand game semantics. In particular, any realizer of an implication-and-negation-free arithmetical formula embodies a winning recursive strategy for the 1-Backtracking version of Tarski games. We also give examples of realizer and winning strategy extraction for some classical proofs. Secondly, we extend our notion of realizability to a total recursive learning based realizability and show that the notion is complete with respect to 1-Backtracking Coquand game semantics.</div></div> (<a href="1BackFull.pdf">pdf</a>) <br><br> <li> Aschieri<br> <i>A Constructive Analysis of Learning in Peano Arithmetic</i> <br>Annals of Pure and Applied to Logic, 2011 <div class="quotetitle"><input type="button" value="Abstract" onclick="showhide(this);" ></div> <div class="quotecontent"><div style="display: none;"> We give a constructive analysis of learning as it arises in various computational interpretations of classical Peano Arithmetic, such as Aschieri and Berardi learning based realizability, Avigad's update procedures and epsilon substitution method. In particular, we show how to compute in Godel's system T upper bounds on the length of learning processes, which are themselves represented inT through learning based realizability. The result is achieved by the introduction of a new non standard model of Godel's T, whose new basic objects are pairs of non standard natural numbers (convergent sequences of natural numbers) and moduli of convergence, where the latter are objects giving constructive information about the former. As foundational corollary, we obtain that that learning based realizability is a constructive interpretation of Heyting Arithmetic plus excluded middle over Sigma_1^0 formulas (for which it was designed) and of all Peano Arithmetic when combined with Godel's double negation translation. As byproduct of our approach, we also obtain a new proof of Avigad's theorem for update procedures and thus of termination of epsilon substitution method for PA. </div></div> (<a href="ConstructiveAnalysisLearning.pdf">pdf</a>) <br><br> <li> Aschieri<br> <i>Interactive Learning Based Realizability and 1-Backtracking Games</i> <br>Proceedings of Classical Logic and Computation 2010 (CL&C 2010), Electronic Proceedings in Theoretical Computer Science, vol. 47, 2011 <div class="quotetitle"><input type="button" value="Abstract" onclick="showhide(this);" ></div> <div class="quotecontent"><div style="display: none;"> We prove that interactive learning based classical realizability (introduced by Aschieri and Berardi for first order arithmetic HA+EM1) is sound with respect to Coquand game semantics. In particular, any realizer of an implication-and-negation-free arithmetical formula embodies a winning recursive strategy for the 1-Backtracking version of Tarski games. We also give examples of realizer and winning strategy extraction for some classical proofs. We also sketch some ongoing work about how to extend our notion of realizability in order to obtain completeness with respect to Coquand semantics, when it is restricted to 1-Backtracking games. </div></div> (<a href="1Back.pdf">pdf</a>) <br><br> <li> Aschieri, Berardi<br> <i>Interactive Learning-Based Realizability for Heyting Arithmetic with EM1</i> (Full Version)<br> Logical Methods in Computer Science, vol. 6, issue 3, n. 19, 2010 <div class="quotetitle"><input type="button" value="Abstract" onclick="showhide(this);" ></div> <div class="quotecontent"><div style="display: none;"> We apply to the semantics of Arithmetic the idea of "finite approximation'' used to provide computational interpretations of Herbrand's Theorem, and we interpret classical proofs as constructive proofs (with constructive rules for or, and) over a suitable structure N for the language of natural numbers and maps of Godel's system T. We introduce a new Realizability semantics we call "Interactive learning-based Realizability'', for Heyting Arithmetic plus EM1 (Excluded middle axiom restricted to Sigma^0_1-formulas). Individuals of N evolve with time, and realizers may "interact'' with them, by influencing their evolution. We build our semantics over Avigad's fixed point result, but the same semantics may be defined over different constructive interpretations of classical arithmetic (by Berardi, continuations are used). Our notion of realizability extends intuitionistic realizability and differs from it only in the atomic case: we interpret atomic realizers as "learning agents''. </div></div> (<a href="http://arxiv.org/pdf/1007.1785">pdf</a>) <br><br> <li> Aschieri, Berardi<br> <i>Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1</i><br>Proceedings of Typed Lambda Calculi and Applications 2009 (TLCA 2009), Springer Lecture Notes in Computer Science, vol. 5608, 2009<br> <br><br> <li> Aschieri, Biasi<br> <i>A Term Assignment for Polarized Bi-intuitionistic Logic and its Strong Normalization</i><br> Fundamenta Informaticae, vol. 84, number 2, 2008<br> <div class="quotetitle"><input type="button" value="Abstract" onclick="showhide(this);" ></div> <div class="quotecontent"><div style="display: none;"> We propose a term assignment (let calculus) for Intuitionistic Logic for Pragmatics ILPAC, a polarized sequent calculus which includes ordinary positive intuitionistic logic, its dual and dual negations which allow a formula to  communicate with its dual fragment. We prove the strong normalization property for the term assignment which follows by soundly translating the let calculus into simply typed lambda calculus with pairings and projections. A new and simple proof of strong normalization for the latter is also provided. </div></div> (<a href="PolarizedBiIntuitionisticLogic.pdf">pdf</a>) <br><br> <li> Aschieri<br> <i>Una caratterizzazione dei lambda termini non fortemente normalizzabili </i> <br> Laurea Thesis, October 2007 <br> <a href="TesiAschieri.pdf"> pdf </a></li> <br> <br> </ul> </div> <hr style="width: 100%; height: 2px;"> <div style="text-align: left;"> <p><b>PERSONAL:</b> </p> </div> <hr style="width: 100%; height: 2px;"> [<a href="http://www.pps.jussieu.fr/pi.r2">Group's HOME</a>] [<a href="http://www.pps.jussieu.fr">Research on "Preuves, Programmes et Systèmes"</a>] [<a href="http://www.univ-paris-diderot.fr">HOME</a>] </BODY> </HTML>