Koundinya Vajjha, Avraham Shinnar, Barry M. Trager, Vasily Pestun, Nathan Fulton: CertRL: formalizing convergence proofs for value and policy iteration in Coq. CPP 2021: 18-31