An intuitionistic theory of types with assumptions of high-arity variables
Martin-Löf's intuitionistic theory of types
scientific article; zbMATH DE number 60738