Ordinals and ordinal functions representable in the simply typed lambda calculus
scientific article; zbMATH DE number 1340821