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

    de Muijnck-Hughes, J., Brady, E. C. & Vanderbauwhede, W., 2 Apr 2019, Proceedings Programming Language Approaches to Concurrency- and Communication-cEntric Software, Prague, Czech Republic, 7th April 2019. Martins, F. & Orchard, D. (eds.). Open Publishing Association, p. 47-59 (Electronic Proceedings in Theoretical Computer Science; vol. 291).

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