Proof reflection in Coq

DOI10.1023/A:1021923116629zbMATH Open1012.03018OpenAlexW1611906969MaRDI QIDQ1868509FDOQ1868509

Dimitri Hendriks

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:1021923116629

zbMATH Keywords

reflectionfirst-order logicnatural deductionCoqformalization of logical systemsreduction relation on proof terms

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (2)

• Proof by computation in the Coq system
• A light-weight integration of automated and interactive theorem proving

Uses Software

• Coq

Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• A formal proof in Coq of Lasalle's invariance principle 👍 👎
• A Proof System for MSVL Programs in Coq 👍 👎
• Proof by computation in the Coq system 👍 👎
• Proof theory of reflection 👍 👎
• From Proposition to Program 👍 👎
• Practical Proof Search for Coq by Type Inhabitation 👍 👎
• Ornaments for Proof Reuse in Coq 👍 👎

This page was built for publication: Proof reflection in Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1868509)