Termination of rewriting in the Calculus of Constructions
From MaRDI portal
Publication:4457836
Recommendations
- Rewriting Techniques and Applications
- Definitions by rewriting in the Calculus of Constructions
- Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved
- Consistency and Completeness of Rewriting in the Calculus of Constructions
- Consistency and Completeness of Rewriting in the Calculus of Constructions
Cited in
(23)- Higher-order superposition for dependent types
- Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures
- Termination of dependently typed rewrite rules
- Termination of Fair Computations in Term Rewriting
- A new look at generalized rewriting in type theory
- Normal higher-order termination
- Computer Science Logic
- Termination of combined (rewrite and λ-calculus) systems
- Computer Science Logic
- HORPO with Computability Closure: A Reconstruction
- Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
- Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved
- Inductive consequences in the calculus of constructions
- Definitions by rewriting in the Calculus of Constructions
- Total termination of term rewriting
- Exits in the refinement calculus
- scientific article; zbMATH DE number 7559278 (Why is no real title available?)
- Termination of just/fair computations in term rewriting
- Variants of the basic calculus of constructions
- Rewriting Techniques and Applications
- Consistency and Completeness of Rewriting in the Calculus of Constructions
- Consistency and Completeness of Rewriting in the Calculus of Constructions
- The Computability Path Ordering: The End of a Quest
This page was built for publication: Termination of rewriting in the Calculus of Constructions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4457836)
