Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

Berardi-deLiguoro:TOCL-11 (Article)
Author(s) Stefano Berardi and Ugo de' Liguoro
Title« Interactive realizers. A new approach to program extraction from non constructive proofs »
JournalACM Transactions on Computational Logic
Volume13
Number2
Page(s)11
Year2012
URLhttp://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 EM1-arithmetic. 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.

BibTeX code

@article{Berardi-deLiguoro:TOCL-11,
  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 EM1-arithmetic.
              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},
}


 Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)

Valid HTML 4.01!