Sequential decision problems, dependently typed solutions

Nicola Botta, Cezar Ionescu, Edwin Charles Brady

Research output: Contribution to conferencePaper

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.
Original languageEnglish
Publication statusPublished - 2013
EventCICM 2013: Conference on Intelligent Computer Mathematics - Bath, United Kingdom
Duration: 8 Jul 201312 Jul 2013

Conference

ConferenceCICM 2013: Conference on Intelligent Computer Mathematics
Country/TerritoryUnited Kingdom
CityBath
Period8/07/1312/07/13

Fingerprint

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

Cite this