| A Finitary Subsystem of Polymorphic-calculus (2007) | |||||||||||||
Abstract | |||||||||||||
| We give a finitary normalisation proof for the restriction of system F where we quantify only over first-order type. As an application, the functions representable in this fragment | |||||||||||||
Publication details | |||||||||||||
| |||||||||||||