Compositional computational reflection

DOI10.1007/978-3-319-08970-6_24zbMATH Open1416.68171OpenAlexW2155149821MaRDI QIDQ2879264FDOQ2879264

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

Recommendations

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

zbMATH Keywords

verificationautomationCoqcomputational reflection

Mathematics Subject Classification ID

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

Cited In (8)

• Compositional CompCert
• Auto in Agda. Programming proof search using reflection
• Automatically proving equivalence by type-safe reflection
• Mtac: a monad for typed tactic programming in Coq
• Lightweight proof by reflection using a posteriori simulation of effectful computation
• Extensible and efficient automation through reflective tactics
• Coqpie: an IDE aimed at improving proof development productivity (rough diamond)
• Title not available (Why is that?)

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)