Sequential decision problems, dependently typed solutions

Nicola Botta, Cezar Ionescu, Edwin Charles Brady

Research output: Contribution to conferencePaper

1 Citation (Scopus)
2 Downloads (Pure)


We propose a dependently typed formalization for a simple
class of sequential decision problems. For this class of problems, we im-
plement a generic version of Bellman's backwards induction algorithm
[2] 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
Original languageEnglish
Publication statusPublished - 2013
EventCICM 2013: Conference on Intelligent Computer Mathematics - Bath, United Kingdom
Duration: 8 Jul 201312 Jul 2013


ConferenceCICM 2013: Conference on Intelligent Computer Mathematics
Country/TerritoryUnited Kingdom


Dive into the research topics of 'Sequential decision problems, dependently typed solutions'. Together they form a unique fingerprint.

Cite this