Strongly normalising cut-elimination with strict intersection types

  • Van Bakel S
  • 2


    Mendeley users who have this article in their library.
  • 1


    Citations of this article.


This paper defines reduction on derivations in the strict intersection type assignment system of [2] by generalising cut-elimination, and shows a strong normalisation result for this reduction. Using this result, new proofs are given for the approximation theorem and the characterisation of normalisability using intersection types. © 2003 Published by Elsevier Science B.V.

Author-supplied keywords

  • Cut-elimination
  • Intersection types
  • Lambda calculus
  • Terminatin

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Steffen Van Bakel

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free