Please use this identifier to cite or link to this item: http://hdl.handle.net/1822/1977

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
Lambda-calculus
Termination
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.
TypeArticle
URIhttp://hdl.handle.net/1822/1977
DOI10.1017/S0960129503004122
ISSN0960-1295
1469-8072
Peer-Reviewedyes
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