Please use this identifier to cite or link to this item:

TitleType-based termination of recursive definitions
Author(s)Barthe, Gilles Jacques Denis
Frade, M. J.
Giménez, E.
Pinto, Luís F.
Uustalu, Tarmo
KeywordsType theory
Issue date2004
PublisherCambridge University Press
JournalMathematical Structures in Computer Science
Citation"Mathematical structures in computer science". ISSN 0960-1295. 14:1 (2004) 97-141.
Abstract(s)This paper introduces "lambda-hat", 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 "lambda-G" in which termination is ensured by a syntactic guard condition. The system can, at will, be extended to also support coinductive types and corecursive function definitions.
AccessOpen access
Appears in Collections:CMAT - Artigos em revistas com arbitragem / Papers in peer review journals
DI/CCTC - Artigos (papers)

Files in This Item:
File Description SizeFormat 
TBterm.pdf441,01 kBAdobe PDFView/Open

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID