Program extraction from normalization proofs
scientific article; zbMATH DE number 5013035