Typing total recursive functions in Coq
scientific article; zbMATH DE number 6821863