Compositional Computational Reflection

DOI10.1007/978-3-319-08970-6_24zbMath1416.68171OpenAlexW2155149821MaRDI QIDQ2879264

Thomas Braibant, Gregory Malecha, Adam Chlipala

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

verificationautomationCoqcomputational reflection

Mathematics Subject Classification ID

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

Related Items (5)

Automatically proving equivalence by type-safe reflection ⋮ Auto in Agda ⋮ Mtac: A monad for typed tactic programming in Coq ⋮ Extensible and Efficient Automation Through Reflective Tactics ⋮ CoqPIE: An IDE Aimed at Improving Proof Development Productivity

Uses Software

• Coq

This page was built for publication: Compositional Computational Reflection