Open AccessA Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems
Author(s) -
Frédéric Blanqui
Publication year - 2004
Publication title -
lecture notes in computer science
Language(s) - English
Resource type - Book series
SCImago Journal Rank - 0.249
H-Index - 400
eISSN - 1611-3349
pISSN - 0302-9743
DOI - 10.1007/978-3-540-25979-4_2
Subject(s) - rewriting , computer science , type (biology) , reduction (mathematics) , programming language , order (exchange) , dependent type , algorithm , theoretical computer science , calculus (dental) , mathematics , lambda calculus , biology , medicine , ecology , geometry , dentistry , finance , economics
Several authors devised type-based termination criteria forML-like languages allowing non-structural recursive calls. We extendthese works to general rewriting and dependent types, hence providinga powerful termination criterion for the combination of rewriting and#-reduction in the Calculus of Constructions.1
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom