A direct proof of strong normalization for full constructive second-order logic
scientific article; zbMATH DE number 2148380