Skip to content

Research at St Andrews

Resource-dependent algebraic effects

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

Author(s)

School/Research organisations

Abstract

There has been significant interest in recent months in finding new ways to implement composable and modular effectful programs using handlers of algebraic effects. In my own previous work, I have shown how an algebraic effect system (called effects) can be embedded directly in a dependently typed host language. Using dependent types ought to allow precise reasoning about programs; however, the reasoning capabilities of effects have been limited to simple state transitions which are known at compile-time. In this paper, I show how effects can be extended to support reasoning in the presence of run-time state transitions, where the result may depend on run-time information about resource usage (e.g. whether opening a file succeeded). I show how this can be used to build expressive APIs, and to specify and verify the behaviour of interactive, stateful programs. I illustrate the technique using a file handling API, and an interactive game.
Close

Details

Original languageEnglish
Title of host publicationTrends in Functional Programming
Subtitle of host publication15th International Symposium, TFP 2014, Soesterberg, The Netherlands, May 26-28, 2014. Revised Selected Papers
EditorsJurriaan Hage, Jay McCarthy
Place of PublicationCham
PublisherSpringer
Pages18-33
ISBN (Electronic)9783319146751
ISBN (Print)9783319146744
DOIs
StatePublished - 2014
EventTrends in Functional Programming - Soesterberg, Netherlands
Duration: 26 May 201428 May 2014
Conference number: 15

Publication series

NameLecture Notes in Computer Science (Theoretical Computer Science and General Issues)
PublisherSpringer
Volume8843
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceTrends in Functional Programming
Abbreviated titleTFP 2014
CountryNetherlands
CitySoesterberg
Period26/05/1428/05/14

    Research areas

  • Dependent type, Functional programming, Game state, Game rule, Syntactic sugar

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: 253098126