TY - RPRT TI - Gradual Certified Programming in Coq AU - Éric Tanter AU - Nicolas Tabareau PY - 2015 DO - 10.1145/2816707.2816710 UR - https://arxiv.org/abs/1506.04205 ID - 1506.04205 ER -