| Abstract |
| We propose a realizability interpretation of a system for quantier free arithmetic which is equivalent to the fragment of classical arithmetic without nested quantiers, 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 environment and with each other. We give a categorical presentation of the inter- pretation through the construction of two suitable monads. |
@unpublished{BerdL10,
url = {http://www.di.unito.it/~deligu/papers/InterRealMonads.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 quantiers, 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 environment and with each other.
We give a categorical presentation of the inter- pretation through
the construction of two suitable monads. },
title = {{Interactive Realizers and Monads}},
author = {Stefano Berardi and Ugo de' Liguoro},
year = {2010},
institution = {Universit\'a di Torino},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)
