Encontrado 1 documento, a visualizar página 1 de 1

Characterising strongly normalising intuitionistic terms

This paper gives a characterisation, via intersection types, of the strongly normalising proof-terms of an intuitionistic sequent calculus (where LJ easily embeds). The soundness of the typing system is reduced to that of a well known typing system with intersection types for the ordinary lambdal-calculus. The completeness of the typing system is obtained from subject expansion at root position. Next we use our...