Type ensured termination of recursive definitions

Maria-Joao Frade

University of Minho

Abstract: I shall talk about a type system for terminating recursive functions. The salient feature of this system is its type-based approach to ensure termination through the notion of stage. The calculus is powerful enough to encode many recursive definitions rejected by existing type systems.

Back to schedule.

Marieke Huisman

Last modified: Mon Feb 12 10:29:23 MET 2001