45 citations · 398 across the 36 of their papers we have counts for
1 paper · 2 filters
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen +1
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments.…