Characterising Strongly Normalising Intuitionistic Terms
José Espírito Santo, Jelena Ivetić, Silvia Likavec · Fundamenta Informaticae · 2012
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 w