Termination checking with types
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 38 (2004) no. 4, pp. 277-319.

Voir la notice de l'article dans Numdam

The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces Λ μ + , a lambda-calculus with recursion, inductive types, subtyping and bounded quantification. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm whose soundness is established formally.

DOI : 10.1051/ita:2004015
Classification : 68N15, 68N18, 68Q42
Mots-clés : type-based termination, sized types, inductive types, course-of-value recursion, bidirectional type checking, strong normalization 
@article{ITA_2004__38_4_277_0,
     author = {Abel, Andreas},
     title = {Termination checking with types},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {277--319},
     publisher = {EDP-Sciences},
     volume = {38},
     number = {4},
     year = {2004},
     doi = {10.1051/ita:2004015},
     zbl = {1089.68028},
     mrnumber = {2098193},
     language = {en},
     url = {https://geodesic-test.mathdoc.fr/articles/10.1051/ita:2004015/}
}
TY  - JOUR
AU  - Abel, Andreas
TI  - Termination checking with types
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2004
SP  - 277
EP  - 319
VL  - 38
IS  - 4
PB  - EDP-Sciences
UR  - https://geodesic-test.mathdoc.fr/articles/10.1051/ita:2004015/
DO  - 10.1051/ita:2004015
LA  - en
ID  - ITA_2004__38_4_277_0
ER  - 
%0 Journal Article
%A Abel, Andreas
%T Termination checking with types
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2004
%P 277-319
%V 38
%N 4
%I EDP-Sciences
%U https://geodesic-test.mathdoc.fr/articles/10.1051/ita:2004015/
%R 10.1051/ita:2004015
%G en
%F ITA_2004__38_4_277_0
Abel, Andreas. Termination checking with types. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 38 (2004) no. 4, pp. 277-319. doi : 10.1051/ita:2004015. https://geodesic-test.mathdoc.fr/articles/10.1051/ita:2004015/

Cité par Sources :