Meta-F\textsuperscript{}: proof automation with SMT, tactics, and metaprograms

DOI10.1007/978-3-030-17184-1_2MaRDI QIDQ6091296zbMATH OpenOpenAlexFDO

Authors Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Cătălin Hriţcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy

Publication date 24 November 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-17184-1_2

zbMATH Keywords

metaprogrammingprogram verificationproof assistantsSMT solverstacticsverification conditions

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Tactics and certificates in Meta Dedukti
• Mtac: a monad for typed tactic programming in Coq
• Mtac: a monad for typed tactic programming in Coq
• Extensible and efficient automation through reflective tactics
• Dependent types and multi-monadic effects in \(\mathrm{F}^*\)

Cited in

(2)

• SAT solving for variants of first-order subsumption
• A mechanically verified garbage collector for OCaml

This page was built for publication: Meta-F\textsuperscript{\(\star\)}: proof automation with SMT, tactics, and metaprograms

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