 Intuitionistic systems have inspired a variety of interpretations, including Beth’s tableaux, Rasiowa and Sikorski’s topological models, Heyting algebras, formulas-as-types, Kleene’s recursive realizabilities, the Kleene and Aczel slashes, and models based on sheafs and topoi. Of all these interpretations Kripke’s [1965] possible-world semantics, with respect to which intuitionistic predicate logic is sound and complete, most resembles classical model theory. Recursive realizability interpretations, on the other hand, attempt to effectively implement the B-H-K explanation of intuitionistic truth.