A Behavioural Model for Klop's Calculus
Mariangiola Dezani-Ciancaglini, Makoto Tatsuta · Electronic Notes in Theoretical Computer Science · 2007
A model characterising strong normalisation for Klop's extension of λ-calculus is presented. The main technical tools for this result are an inductive definition of strongly normalising terms of Klop's calculus and an intersection type system for terms of Klop's calculus.