@techreport{RR-04-20,
  abstract = "The size-change termination principle \cite is a simple criterion for program termination, originally described for first-order functional programs. A program is size-change terminating if any infinite call sequence would result in an infinite decrease of a well-founded parameter. This is a powerful and simple termination analysis, so that it identifies termination for a substantial and natural class of programs. In addition, its extensional power is the class of mutual recursive functions.<p>The ideas underlying the size-change termination analysis have been applied recently to develop a termination analysis for the pure untyped lambda calculus. Again, this is a powerful method, proving termination of lambda expressions containing even the Y fixpoint combinator.</p><p>We bridge the gap between the two analyses by developing a termination analysis of a call-by-value, higher order functional language. This is an application of the ideas used in the lambda calculus analysis, which it subsumes. It is also a useful step in applying this analysis to real functional programs.</p>",
  author = "Damien Sereni",
  institution = "Oxford University Computing Laboratory",
  month = "October",
  number = "RR-04-20",
  title = "Size-Change Termination of Higher-Order Functional Programs",
  year = "2004",
}