A proof of the normal form theorem for the closed terms of Girard's system F by means of computability
Silvio Valentini · Mathematical logic quarterly · 1993
Abstract In this paper a proof of the normal form theorem for the closed terms of Girard's system F is given by using a computability method à la Tait. It is worth noting that most of the standard consequences of the normal form theorem can be obtained using this version of the theorem as well. From the proof‐theoretical point of view the interest of the proof is that the definition of computable derivation here used does not seem to be well founded. MSC: 03F05, 03B15.