Abstract
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
problems.
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
problems.
Original language | English |
---|---|
Publication status | Published - 2013 |
Event | CICM 2013: Conference on Intelligent Computer Mathematics - Bath, United Kingdom Duration: 8 Jul 2013 → 12 Jul 2013 |
Conference
Conference | CICM 2013: Conference on Intelligent Computer Mathematics |
---|---|
Country/Territory | United Kingdom |
City | Bath |
Period | 8/07/13 → 12/07/13 |