Skip to content

Research at St Andrews

Sequential decision problems, dependently typed solutions

Research output: Contribution to conferencePaper

Author(s)

Nicola Botta, Cezar Ionescu, Edwin Charles Brady

School/Research organisations

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.
Close

Details

Original languageEnglish
StatePublished - 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
CountryUnited Kingdom
CityBath
Period8/07/1312/07/13

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Type driven development of concurrent communicating systems

    Brady, E. C. 7 Jul 2017 In : Computer Science. 18, 3, 22 p., 1413

    Research output: Contribution to journalArticle

  2. Sequential decision problems, dependent types and generic solutions

    Botta, N., Jansson, P., Ionescu, C., Christiansen, D. & Brady, E. C. 17 Mar 2017 In : Logical Methods in Computer Science. 13, 1, 23 p., 7

    Research output: Contribution to journalArticle

  3. Type-driven development with Idris

    Brady, E. C. Mar 2017 Shelter Island: Manning Publications Co.480 p.

    Research output: Book/ReportBook

  4. Automatically proving equivalence by type-safe reflection

    Slama, F. & Brady, E. C. 2017 Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings. Geuvers, H., England, M., Hasan, O., Rabe, F. & Teschke, O. (eds.). Cham: Springer, p. 40-55 (Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence); vol. 10383)

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  5. Elaborator reflection: extending Idris in Idris

    Christiansen, D. & Brady, E. C. 4 Sep 2016 Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. New York: ACM, p. 284-297

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

ID: 62964317