 One of the reasons for the widespread use of intuitionistic logic is that it is well-behaved both from the proof-theoretic as the model-theoretic point of view. There exist a great many proof systems for it, such as Gentzen calculi and natural deduction systems, as well as various forms of semantics, such as Kripke models, Beth models, Heyting algebras, topological semantics and categorical models. Several of these semantics are, however, only classical means to study intuitionistic logic, for it can be shown that an intuitionistic completeness proof with respect to them cannot exist (Kreisel 1962). It has, however, been shown that there are alternative but a little less natural models with respect to which completeness does hold constructively (Veldman 1976). The constructive character of intuitionistic logic becomes particularly clear in the Curry-Howard isomorphism that establishes a correspondence between derivations in the logic and terms in simply typed \(\lambda\)-calculus, that is, between proofs and computations. The correspondence preserves structure in that reduction of terms correspond to normalization of proofs. 