Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
- 1 January 2006
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
- p. 105-119
- https://doi.org/10.1007/11916277_8
Abstract
No abstract availableKeywords
Other Versions
This publication has 17 references indexed in Scilit:
- On the Confluence of λ-Calculus with Conditional RewritingLecture Notes in Computer Science, 2006
- Practical Inference for Type-Based Termination in a Polymorphic SettingLecture Notes in Computer Science, 2005
- Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size AnnotationsLecture Notes in Computer Science, 2005
- Termination checking with typesRAIRO - Theoretical Informatics and Applications, 2004
- A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite SystemsLecture Notes in Computer Science, 2004
- Rewriting Modulo in Deduction ModuloLecture Notes in Computer Science, 2003
- Termination and Productivity Checking with Continuous TypesLecture Notes in Computer Science, 2003
- Termination and Confluence of Higher-Order Rewrite SystemsLecture Notes in Computer Science, 2000
- Definitions by rewriting in the Calculus of ConstructionsMathematical Structures in Computer Science, 1999
- Type-based termination of recursive definitionsMathematical Structures in Computer Science, 1999