Treffer: A type-based termination criterion for dependently-typed higher-order rewrite systems
Title:
A type-based termination criterion for dependently-typed higher-order rewrite systems
Authors:
Source:
RTA 2004 : rewriting techniques and applications (Aachen, 3-5 June 2004)Lecture notes in computer science. :24-39
Publisher Information:
Berlin: Springer, 2004.
Publication Year:
2004
Physical Description:
print, 26 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Théorie programmation, Programming theory, Langage ML, ML language, Problème terminaison, Termination problem, Problema terminación, Réécriture, Rewriting, Reescritura, Système réécriture, Rewriting systems
Document Type:
Konferenz
Conference Paper
File Description:
text
Language:
English
Author Affiliations:
LORIA & INRIA, 615 rue du Jardin Botanique, BP 101, 54602 Villers-lès-Nancy, France
ISSN:
0302-9743
Rights:
Copyright 2004 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.15851901
Database:
PASCAL Archive
Weitere Informationen
Several 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 β-reduction in the Calculus of Constructions.