Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation

DOI10.1007/978-3-642-39634-2_8zbMath1317.68205OpenAlexW205472424MaRDI QIDQ5327337

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

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (5)

Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker ⋮ How to get more out of your oracles ⋮ Formally proving size optimality of sorting networks ⋮ Mtac: A monad for typed tactic programming in Coq ⋮ 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