References
A. G. Dragalin
A completeness theorem for higher-order intuitionistic logic: an intuitionistic proof
1987
in: Mathematical logic and its applications, Dordrecht : Springer
Cut-elimination theorem for higher-order classical logic: an intuitionistic proof
1987
in: Mathematical logic and its applications, Dordrecht : Springer