A compact kernel for the calculus of inductive constructions
scientific article; zbMATH DE number 5637281