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 A 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.
A proof of the normal form theorem for the closed terms of Girard's System F
VALENTINI, SILVIO
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 A 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.File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
