Thomas Letan, Yann Régis-Gianas: FreeSpec: specifying, verifying, and executing impure computations in Coq. CPP 2020: 32-46