Journal article
Termination Casts: A Flexible Approach to Termination with General Recursion
Electronic proceedings in theoretical computer science, Vol.43(43), pp.76-93
12/22/2010
DOI: 10.4204/EPTCS.43.6
Abstract
This paper proposes a type-and-effect system called T-eq down arrow, 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 T-eq down arrow to a logical theory of termination for general recursive, simply typed functions. Every typing judgment of T-eq down arrow is translated to a theorem expressing the appropriate termination property of the computational part of the T-eq down arrow term.
Details
- Title: Subtitle
- Termination Casts: A Flexible Approach to Termination with General Recursion
- Creators
- Aaron Stump - University of IowaVilhelm Sjoeberg - Univ Penn, Comp & Informat Sci, Philadelphia, PA 19104 USAStephanie Weirich - University of Pennsylvania
- Resource Type
- Journal article
- Publication Details
- Electronic proceedings in theoretical computer science, Vol.43(43), pp.76-93
- DOI
- 10.4204/EPTCS.43.6
- ISSN
- 2075-2180
- eISSN
- 2075-2180
- Publisher
- Open Publ Assoc
- Number of pages
- 18
- Grant note
- 0702545; 0910510; 0910786 / U.S. National Science Foundation; National Science Foundation (NSF)
- Language
- English
- Date published
- 12/22/2010
- Academic Unit
- Computer Science
- Record Identifier
- 9984410842202771
Metrics
5 Record Views