Name for type theories derived from Per Martin-Löf’s work. martin-lof1975-intuitionistic-predicative martin-lof1984-mltt. Martin Lof’s Logical Framework The design is that type formers can be added to the base system, by just adding new constants in the (tarski) universe . The base logical framework, has just -types, and a few other constructs. nordstrom-petersson-smith1990-mltt. The Alf system magnusson1994-alf-mltt is based on the Logical Framework, that allows for the definition of types in set simply by giving their constructors. Functions on the types are then defined by pattern-matching over the constructors. hoffmann1997-dependent-types (sect 2.2.2).