Type-based termination of recursive definitions

被引：60
作者：
Barthe, G
Frade, MJ
Giménez, E
Pinto, L
Uustalu, T
机构：
[1] INRIA Sophia Antipolis, F-06902 Sophia Antipolis, France
[2] Univ Minho, Dept Informat, P-4710057 Braga, Portugal
[3] Univ Republica, Inst Computac, Montevideo 11300, Uruguay
[4] Univ Minho, Dept Matemat, P-4710057 Braga, Portugal
[5] Univ Minho, Dept Informat, P-4710057 Braga, Portugal
[6] Inst Cybernet, EE-12618 Tallinn, Estonia
来源：
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE | 2004年 / 14卷 / 01期
关键词：
D O I：
10.1017/S0960129503004122
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
This paper introduces lambda<^>, 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.
引用
收藏
页码：97 / 141
页数：45
相关论文
共 49 条
[1]   A predicative analysis of structural recursion [J].
Abel, A ;
Altenkirch, T .
JOURNAL OF FUNCTIONAL PROGRAMMING, 2002, 12 :1-41
[2]  
Abel A, 2000, LNCS, V1956, P1, DOI [10. 1007/3- 540- 44557-9 1, DOI 10.1007/3-540-44557-91]
[3]  
ALTENKIRCH T, 1999, SPRINGER VERLAGE LEC, V1584, P343
[4]  
Amadio RM, 1998, LECT NOTES COMPUT SC, V1378, P48, DOI 10.1007/BFb0053541
[5]  
BAC A, 1998, MEMOIRE DEA
[6]  
BARRAS B, 1999, THESIS U PARIS 7
[7]   Inductive-data-type systems [J].
Blanqui, F ;
Jouannaud, JP ;
Okada, M .
THEORETICAL COMPUTER SCIENCE, 2002, 272 (1-2) :41-68
[8]  
CHIN WN, 2001, HIGHER ORDER SYMBOLI, V14, P261
[9]  
Coquand T, 1994, LECT NOTES COMPUT SC, V880, P60
[10]  
COQUAND T, 1990, LECT NOTES COMPUT SC, V417, P50
12345