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 条
[11]  
COQUAND T, 1992, INF P WORKSH TYP PRO, P71
[12]  
CORNES C, 1997, THESIS U PARIS 7
[13]   Abstract interpretation [J].
Cousot, P .
ACM COMPUTING SURVEYS, 1996, 28 (02) :324-328
[14]  
Dybjer P., 1994, Formal Aspects of Computing, V6, P440, DOI 10.1007/BF01211308
[15]  
ELBERS H, 1998, THESIS TU EINDHOVEN
[16]  
Geuvers Herman, 1992, INFORMAL P WORKSHOP, P193
[17]  
Giesl J, 1998, APPL LOG SER, V10, P135
[18]  
GIMENEZ E, 1996, THESIS EOCLE NORMALE
[19]  
GIMENEZ E, 1998, SPRINGER VERLAG LECT, V1443, P397
[20]  
Gimenez Eduardo, 1995, Types for Proofs and Programs, International Workshop TYPES'94, Bastad, Sweden, June 6-10, 1994, Selected Papers, DOI DOI 10.1007/3-540-60579-7_3
12345