A type-based termination criterion for dependently-typed higher-order rewrite systems

Simple item page
dc.creatorBlanqui, Frederic
dc.date2006-10-11
dc.date.accessioned2026-07-07T07:27:51Z
dc.date.available2026-07-07T07:27:51Z
dc.descriptionSeveral authors devised type-based termination criteria for ML-like languages allowing non-structural recursive calls. We extend these works to general rewriting and dependent types, hence providing a powerful termination criterion for the combination of rewriting and beta-reduction in the Calculus of Constructions.
dc.descriptionColloque avec actes et comité de lecture. internationale
dc.identifierhttps://arxiv.org/abs/cs/0610062
dc.identifierhttp://arxiv.org/abs/cs/0610062
dc.identifierDans 15th International Conference on Rewriting Techniques and Applications - RTA'04 (2004) 15 p
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/117521
dc.subjectLogic in Computer Science
dc.subjectProgramming Languages
dc.titleA type-based termination criterion for dependently-typed higher-order rewrite systems
dc.typetext

Files

Collections

arXiv