CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq

Open in new window