  We investigate a framework of Krivine realizability with I/O effects, and
present a method of associating realizability models to specifications on the
I/O behavior of processes, by using adequate interpretations of the central
concepts of `pole' and `proof-like term'. This method does in particular allow
to associate realizability models to computable functions.
  Following recent work of Streicher and others we show how these models give
rise to triposes and toposes.
