Definitions by rewriting in the Calculus of Constructions
From MaRDI portal
Publication:4657751
DOI10.1017/S0960129504004426zbMath1060.03046MaRDI QIDQ4657751
Publication date: 14 March 2005
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Related Items (11)
Size-based termination of higher-order rewriting ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ The Computability Path Ordering: The End of a Quest ⋮ Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules ⋮ A domain model characterising strong normalisation ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On the confluence of lambda-calculus with conditional rewriting ⋮ Unnamed Item ⋮ CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates ⋮ On the Relation between Sized-Types Based Termination and Semantic Labelling
Uses Software
This page was built for publication: Definitions by rewriting in the Calculus of Constructions
