Type-based termination of recursive definitions

G. Barthe, M. J. Frade, E. Giménez, L. Pinto, T. Uustalu

Research output: Contribution to journalArticlepeer-review

78 Citations (Scopus)


This paper introduces X a simply typed lambda calculus supporting inductive types and recursive function definitions with termination ensured by types. The system is shown to enjoy subject reduction, strong normalisation of typable terms and to be stronger than a related system ; in which termination is ensured by a syntactic guard condition. The system can, at will, be extended to support coinductive types and corecursive function definitions also.

Original languageEnglish
Pages (from-to)97-141
Number of pages45
JournalMathematical Structures in Computer Science
Issue number1
Publication statusPublished - 2004


Dive into the research topics of 'Type-based termination of recursive definitions'. Together they form a unique fingerprint.

Cite this