CertRL: formalizing convergence proofs for value and policy iteration in Coq.

Koundinya Vajjha, Avraham Shinnar, Barry M. Trager, Vasily Pestun, Nathan Fulton

Browse the full CPP paper archive.