Termination Casts: A Flexible Approach to Termination with General Recursion

This paper proposes a type-and-effect system called Teq, which distinguishes terminating terms and total functions from possibly diverging terms and partial functions, for a lambda calculus with general recursion and equality types. The central idea is to include a primitive type-form "Terminates t", expressing that term t is terminating; and then allow terms t to be coerced from possibly diverging to total, using a proof of Terminates t. We call such coercions termination casts, and show how to implement terminating recursion using them. For the meta-theory of the system, we describe a translation from Teq to a logical theory of termination for general recursive, simply typed functions. Every typing judgment of Teq is translated to a theorem expressing the appropriate termination property of the computational part of the Teq term.

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Aaron Stump, Vilhelm Sjöberg, Stephanie Weirich
• Keywords: Appropriate Termination Property, Coercions Termination, CORR 2010, Education, Teq Term