Certifying Term Rewriting Proofs in ELAN

DOI10.1016/S1571-0661(04)00295-6zbMath1268.68102MaRDI QIDQ2841249

Quang Huy Nguyen

Publication date: 24 July 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Uses Software

• Coq
• ELAN
• Nuprl

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Complexity of matching problems
• The calculus of constructions
• Conditional rewriting logic as a unified model of concurrency
• Theorem proving modulo
• Optimized encodings of fragments of type theory in first-order logic
• Confluence properties of weak and strong calculi of explicit substitutions
• Explicit substitutions

This page was built for publication: Certifying Term Rewriting Proofs in ELAN