Compositional computational reflection

DOI10.1007/978-3-319-08970-6_24MaRDI QIDQ2879264zbMATH OpenOpenAlexFDO

Authors Gregory Malecha, Adam Chlipala, Thomas Braibant

Publication date 8 September 2014

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL http://nrs.harvard.edu/urn-3:HUL.InstRepos:12537617

zbMATH Keywords

automationcomputational reflectionCoqverification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 2185723
• Theorem Proving in Higher Order Logics
• Computational reflection via mechanized logical deduction
• Extensible and efficient automation through reflective tactics
• Reflection principles in computational logic

Cited in

(9)

• Automatically proving equivalence by type-safe reflection
• Extensible and efficient automation through reflective tactics
• Compositional CompCert
• Coqpie: an IDE aimed at improving proof development productivity (rough diamond)
• Auto in Agda. Programming proof search using reflection
• Lightweight proof by reflection using a posteriori simulation of effectful computation
• Mtac: a monad for typed tactic programming in Coq
• scientific article; zbMATH DE number 2219520 (Why is no real title available?)
• Equations for hereditary substitution in Leivant's predicative system F: a case study

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Compositional computational reflection

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