ETD

• Polymorphism
• System-F
• Type-systems

The language MLF is an extension of System-F that permits robust first-order partial type inference with second-order polymorphism.
We propose an extension of MLF's graphical presentation with higher-order types and reduction at the type level as in System-Fω. As inference of higher-order types won't be possible in general, the extension introduces System-F-style explicit type abstractions and type application into MLF.