External rewriting for skeptical proof assistants

DOI10.1023/A:1021975117537zbMath1064.68048OpenAlexW1582156629MaRDI QIDQ1868511

Claude Kirchner, Quang Huy Nguyen, Hélène Kirchner

Publication date: 27 April 2003

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1021975117537

zbMATH Keywords

term rewritingtype theoryproof assistantcertification\(\rho\)-calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items (4)

Tool-assisted specification and verification of typed low-level languages ⋮ A \(\rho\)-calculus of explicit constraint application ⋮ Twenty years of rewriting logic ⋮ Tactics for Reasoning Modulo AC in Coq

Uses Software

• Coq
• ELAN
• Gandalf

This page was built for publication: External rewriting for skeptical proof assistants