In this paper, Krivine describes his machine and maps it to classical logic (he implements something like call/cc at the end).
Only, I have trouble understanding how he establishes this correspondence without specifying a type system. Is it purely by talking about input/output rather than type/inhabitant? I saw that the realizability interpretation was about that, but I don't really understand it.