A Behavioural Model for Klop's Calculus

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. Key words: Klop’s extension of λ-calculus, strong normalisation, intersection types.

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Mariangiola Dezani-Ciancaglini, Makoto Tatsuta
• Keywords: ENTCS 2007, Intersection Types, Klop’s Extension, Strong Normalisation