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
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
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. Value-dependent session design in a dependently typed language

    de Muijnck-Hughes, J., Vanderbauwhede, W. & Brady, E. C., 7 Apr 2019, Electronic Proceedings in Theoretical Computer Science. Open Publishing Association

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

  2. Subtype polymorphism à la carte via machine learning on dependent types

    Swan, J., Johnson, C. G. & Brady, E. C., 16 Jul 2018, Companion Proceedings for the ISSTA/ECOOP 2018 Workshops. New York, NY: Association for Computing Machinery, Inc, p. 14-16 3 p.

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

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

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

  5. Type-driven development with Idris

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

    Research output: Book/ReportBook

ID: 62964317