A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems
Author:
- 1 January 2004
- book chapter
- Published by Springer Nature in Lecture Notes in Computer Science
- p. 24-39
Abstract
No abstract availableKeywords
All Related Versions
This publication has 17 references indexed in Scilit:
- Type-based termination of recursive definitionsMathematical Structures in Computer Science, 2004
- Rewriting Modulo in Deduction ModuloLecture Notes in Computer Science, 2003
- Inductive Types in the Calculus of Algebraic Constructions2003
- Termination and Productivity Checking with Continuous TypesLecture Notes in Computer Science, 2003
- Inductive-data-type systemsTheoretical Computer Science, 2002
- Termination and Confluence of Higher-Order Rewrite Systems2000
- Proof Normalization Modulo1999
- Termination of Nested and Mutually Recursive AlgorithmsJournal of Automated Reasoning, 1997
- Natural terminationTheoretical Computer Science, 1995
- The calculus of constructionsInformation and Computation, 1988