  We propose a logic of interactive proofs as a framework for an intuitionistic
foundation for interactive computation, which we construct via an interactive
analog of the Goedel-McKinsey-Tarski-Artemov definition of Intuitionistic Logic
as embedded into a classical modal logic of proofs, and of the Curry-Howard
isomorphism between intuitionistic proofs and typed programs. Our interactive
proofs effectuate a persistent epistemic impact in their intended communities
of peer reviewers that consists in the induction of the (propositional)
knowledge of their proof goal by means of the (individual) knowledge of the
proof with the interpreting reviewer. That is, interactive proofs effectuate a
transfer of propositional knowledge (knowable facts) via the transmission of
certain individual knowledge (knowable proofs) in multi-agent distributed
systems. In other words, we as a community can have the formal common knowledge
that a proof is that which if known to one of our peer members would induce the
knowledge of its proof goal with that member. Last but not least, we prove
non-trivial interactive computation as definable within our simply typed
interactive Combinatory Logic to be nonetheless equipotent to non-interactive
computation as defined by simply typed Combinatory Logic.
