131 citations · 132 across the 3 of their papers we have counts for
1 paper · 1 filter
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…