Mathematical Intuitionism: Introduction to Proof Theory
Albert G. Dragalin · Translations of mathematical monographs · 1988
Logic Arithmetic Algebraic models Analysis Eliminability of cuts in the intuitionistic simple theory of types in the form of a sequent calculus with extensionality Appendix A: An algebraic approach to models of realizability type Appendix B: A strong form of the normalization theorem.