 Troelstra’s [1973], Beeson’s [1985] and Troelstra and van Dalen’s [1988] (with  corrections)  stand out as the most comprehensive studies of intuitionistic and semi-intuitionistic formal theories, using both constructive and classical methods, with useful bibliographies. Troelstra and Schwichtenberg [2000] presents the proof theory of classical, intuitionistic and minimal logic in parallel, focusing on sequent systems. Troelstra’s [1998] presents formulas-as-types and (Kleene and Aczel) slash interpretations for propositional and predicate logic, as well as abstract and concrete realizabilities for a multitude of applications. Martin-Löf’s constructive theory of types [1984] (cf. Section 3.4 of the entry on  constructive mathematics)  provides another general framework within which intuitionistic reasoning continues to develop.