We’ve just shipped the camera ready version of the following paper to PLMMS 2013:

Sequential decision problems, dependently typed solutions

Nicola Botta, Cezar Ionescu, Edwin Brady

We propose a dependently typed formalization for a simple class of sequential decision problems. For this class of problems, we implement a generic version of Bellman’s backwards induction algorithm and a machine checkable proof that the proposed implementation is correct. The formalization is generic. It is presented in Idris, but it can be easily translated to other dependently-typed programming languages. We conclude with an informal discussion of the problems we have faced in extending the formalization to generic monadic sequential decision problems.

You can find the full paper here.