131 citations · 132 across the 3 of their papers we have counts for
Showing cs.PLShow all
2 papers · 1 filter
cs.PL2019★ 131 cited
Interaction Trees: Representing Recursive and Impure Programs in Coq
Li-yao Xia, Yannick Zakowski, Paul He +4
"Interaction trees" (ITrees) are a general-purpose data structure for representing the behaviors of recursive programs that interact with their environments. A coinductive variant…
cs.PL2013★ 1 cited
MirrorShard: Proof by Computational Reflection with Verified Hints
Gregory Malecha, Adam Chlipala, Thomas Braibant +2
We describe a method for building composable and extensible verification procedures within the Coq proof assistant. Unlike traditional methods that rely on run-time generation and…