Proof certificates for equality reasoning

DOI10.1016/j.entcs.2016.06.007zbMath1394.68350OpenAlexW2463700520WikidataQ113317682 ScholiaQ113317682MaRDI QIDQ1744408

Zakaria Chihani, Dale A. Miller

Publication date: 23 April 2018

Full work available at URL: https://doi.org/10.1016/j.entcs.2016.06.007

zbMATH Keywords

proof checkingequational proofsproof certificatesrewriting proofs

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Structure of proofs (03F07)

Related Items

Proof checking and logic programming, A semantic framework for proof evidence

Uses Software

• CeTA

Cites Work

• Unnamed Item
• Unnamed Item
• Focusing and polarization in linear, intuitionistic, and classical logics
• Counterexamples to termination for the direct sum of term rewriting systems
• Autarkic computations in formal proofs
• Uniform proofs as a foundation for logic programming
• Programming with Higher-Order Logic
• A Proposal for Broad Spectrum Proof Certificates
• Certification of Termination Proofs Using CeTA
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• Logic Programming with Focusing Proofs in Linear Logic
• A framework for defining logics
• Foundational Proof Certificates in First-Order Logic
• Introduction to generalized type systems
• General models, descriptions, and choice in type theory
• Automated Deduction – CADE-19