BerardideLiguoro:TOCL11 (Article)

Author(s)  Stefano Berardi and Ugo de' Liguoro 
Title  « Interactive realizers. A new approach to program extraction from non constructive proofs » 
Journal  ACM Transactions on Computational Logic 
Volume  13 
Number  2 
Page(s)  11 
Year  2012 
URL  http://tocl.acm.org/accepted/451deLiguoro.pdf 
Abstract 
We propose a realizability interpretation of a system for quantier free arithmetic which is equivalent to the fragment of classical arithmetic without nested quantifiers, called here EM1arithmetic. We interpret classical proofs as interactive learning strategies, namely as processes going through several stages of knowledge and learning by interacting with the “nature”, represented by the standard interpretation of closed atomic formulas, and with each other. We obtain in this way a program extraction method by proof interpretation, which is faithful w.r.t. proofs, in the sense that it is compositional and that it does not need any translation. 
@article{BerardideLiguoro:TOCL11,
number = {2},
volume = {13},
author = {Stefano Berardi and Ugo de' Liguoro},
url = {http://tocl.acm.org/accepted/451deLiguoro.pdf},
tag = {{ACM Transactions on Computational Logic}},
title = {{Interactive realizers. A new approach to program extraction from non
constructive proofs}},
abstract = {We propose a realizability interpretation of a system for quantier
free arithmetic which is equivalent to the fragment of classical
arithmetic without nested quantifiers, called here EM1arithmetic.
We interpret classical proofs as interactive learning strategies,
namely as processes going through several stages of knowledge and
learning by interacting with the “nature”, represented by the
standard interpretation of closed atomic formulas, and with each
other. We obtain in this way a program extraction method by proof
interpretation, which is faithful w.r.t. proofs, in the sense that
it is compositional and that it does not need any translation.},
year = {2012},
pages = {11},
journal = {ACM Transactions on Computational Logic},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)