Meta programming on the proof level

MaRDI QIDQ3631203zbMATH OpenFDO

Authors Gergely Dévai

Publication date 5 June 2009

zbMATH Keywords

computer aided proof generation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 140006
• Towards Formal Proof Script Refactoring
• Auto in Agda. Programming proof search using reflection
• Writing programs that construct proofs
• Programming language elements for proof construction

Cited in

(6)

• The \textsc{MetaCoq} project
• Metamath Zero: designing a theorem prover prover
• Program Logics for Homogeneous Meta-programming
• scientific article; zbMATH DE number 4076581 (Why is no real title available?)
• Why untyped nonground metaprogramming is not (much of) a problem
• Verification of meta-interpreters

This page was built for publication: Meta programming on the proof level

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