Termination Analysis with Types Is More Accurate

Abstract. In this paper we show how we can use size and groundness analyses lifted to regular and (polymorphic) Hindley/Milner typed programs to determine more accurate termination of (type correct) programs. Type information for programs may be either inferred automatically or declared by the programmer. The analysis of the typed logic programs is able to completely reuse a framework for termination analyntyped logic programs by using abstract compilation of the type ion. We show that our typed termination analysis is uniformly more accurate than untyped termination analysis for regularly typed programs, and demonstrate how it is able to prove termination of programs which the untyped analysis can not.

• Type: Conference
• Year: 2003
• Where: ICLP
• Authors: Vitaly Lagoon, Frédéric Mesnard, Peter J. Stuckey
• Keywords: Hindley/Milner Typed Programs, ICLP 2003, Programming Languages, Typed Programs, Typed Termination Analysis