Termination Casts: A Flexible Approach to Termination with General Recursion

Aaron Stump, Vilhelm Sjöberg, Stephanie Weirich

This paper proposes a type-and-effect system called Teqt, which distinguishes terminating terms and total functions from possibly diverging terms and partial functions, for a lambd…