Lightweight proof by reflection using a posteriori simulation of effectful computation

DOI10.1007/978-3-642-39634-2_8zbMATH Open1317.68205OpenAlexW205472424MaRDI QIDQ5327337FDOQ5327337

Authors: Guillaume Claret, Lourdes del Carmen González Huesca, Yann Régis-Gianas, Beta Ziliani 

Publication date: 7 August 2013

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

Full work available at URL: https://doi.org/10.1007/978-3-642-39634-2_8

Recommendations

• Extensible and efficient automation through reflective tactics
• Auto in Agda. Programming proof search using reflection
• scientific article; zbMATH DE number 2185723
• Theorem Proving in Higher Order Logics
• Compositional computational reflection

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Cited In (6)

• How to get more out of your oracles
• Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
• Mtac: a monad for typed tactic programming in Coq
• Formalizing size-optimal sorting networks: extracting a certified proof checker
• Formally proving size optimality of sorting networks
• Extensible and efficient automation through reflective tactics

Uses Software

• Coq

This page was built for publication: Lightweight proof by reflection using a posteriori simulation of effectful computation

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