Encontrados 2 documentos, a visualizar página 1 de 1
Characterising strongly normalising intuitionistic terms
Espírito Santo, José; Ivetic, J,; Likavec, SilviaThis 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...
Characterising strongly normalising intuitionistic sequent terms
Espírito Santo, José; Ghilezan, S.; Ivetic, J.This paper gives a characterisation, via intersection types, of the strongly normalising 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 lambda-calculus. The completeness of the typing system is obtained from subject expansion at root position. This paper's sequent t...
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||