The extended calculus of constructions (ECC) with inductive types
scientific article; zbMATH DE number 64881