| 2 1 (2007) | |||||||||||||
Abstract | |||||||||||||
| Abstract. We give a nitary normalisation proof for the restriction of system F where we quantify only over rst-order type. As an application, the functions representable in this fragment are exactly the ones provably total in Peano Arithmetic. This is inspired by the reduction of | |||||||||||||
Publication details | |||||||||||||
| |||||||||||||