A. G. Dragalin

, 1987a, A completeness theorem for higher-order intuitionistic logic: an intuitionistic proof, in D. G. Skordev (ed.), Mathematical logic and its applications, Dordrecht, Springer, pp. 107-124.

, 1987b, Cut-elimination theorem for higher-order classical logic: an intuitionistic proof, in D. G. Skordev (ed.), Mathematical logic and its applications, Dordrecht, Springer, pp. 243-251.