Show simple item record

dc.contributor.advisorMcKinna, James
dc.contributor.advisorStark, Ian
dc.contributor.authorMcLaughlin, Craig
dc.date.accessioned2020-08-31T15:44:44Z
dc.date.available2020-08-31T15:44:44Z
dc.date.issued2020-07-25
dc.identifier.urihttps://hdl.handle.net/1842/37236
dc.identifier.urihttp://dx.doi.org/10.7488/era/537
dc.description.abstractThis thesis studies relational reasoning techniques for FRANK, a strict functional language supporting algebraic effects and their handlers, within a general, formalised approach for completely characterising observational equivalence. Algebraic effects and handlers are an emerging paradigm for representing computational effects where primitive operations, which give rise to an effect, are primary, and given semantics through their interpretation by effect handlers. FRANK is a novel point in the design space because it recasts effect handling as part of a generalisation of call-by-value function application. Furthermore, FRANK generalises unary effect handlers to the n-ary notion of multihandlers, supporting more elegant expression of certain handlers. There have been recent efforts to develop sound reasoning principles, with respect to observational equivalence, for languages supporting effects and handlers. Such techniques support powerful equational reasoning about code, such as substitution of equivalent sub-terms (‘equals for equals’) in larger programs. However, few studies have considered a complete characterisation of observational equivalence, and its implications for reasoning techniques. Furthermore, there has been no account of reasoning principles for FRANK programs. Our first contribution is a formal reconstruction of a general proof technique, triangulation, for proving completeness results for observational equivalence. The technique brackets observational equivalence between two structural relations, a logical and an applicative notion. We demonstrate the triangulation proof method for a pure simply-typed λ-calculus. We show that such results are readily formalisable in an implementation of type theory, specifically AGDA, using state-of-the-art technology for dealing with syntaxes with binding. Our second contribution is a calculus, ELLA, capturing the essence of FRANK’s novel design. In particular, ELLA supports binary handlers and generalises function application to incorporate effect handling. We extend our triangulation proof technique to this new setting, completely characterising observational equivalence for this calculus. We report on our partial progress in formalising our extension to ELLA in AGDA. Our final contribution is the application of sound reasoning principles, inspired by existing literature, to a variety of ELLA programs, including a proof of associativity for a canonical pipe multihandler. Moreover, we show how leveraging completeness leads, in certain instances, to simpler proofs of observational equivalence.en
dc.contributor.sponsorEngineering and Physical Sciences Research Council (EPSRC)en
dc.language.isoenen
dc.publisherThe University of Edinburghen
dc.relation.hasversionLukas Convent, Sam Lindley, Conor McBride, and Craig McLaughlin. Doo bee doo bee doo. Journal of Functional Programming (special issue on algebraic effects and handlers), 30:e9, 2020. doi:10.1017/S0956796820000039.en
dc.relation.hasversionCraig McLaughlin, James McKinna, and Ian Stark. Triangulating context lemmas. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pp. 102–114, 2018. doi:10.1145/3167081.en
dc.relation.hasversionSam Lindley, Conor McBride, and Craig McLaughlin. Do be do be do. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 500–514, 2017. doi:10.1145/3093333.3009897en
dc.relation.hasversionLukas Convent, Sam Lindley, Conor McBride, and Craig McLaughlin. Frank repository, 2019. https://www.github.com/frank-lang/frank.en
dc.relation.hasversionGeorg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, and Viktor Vafeiadis. Pilsner: A compositionally verified compiler for a higher-order imperative language. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pp. 166–178. ACM, 2015. doi:10.1145/2784731.2784764.en
dc.subjectmodelingen
dc.subjectobservable behaviour of computer programsen
dc.subjecttype-and-effect systemsen
dc.subjectprogram equivalenceen
dc.subjectoptimisationen
dc.subjectrelational reasoning techniquesen
dc.subjectFRANKen
dc.subjectAGDAen
dc.subjecttriangulation proof techniqueen
dc.titleRelational reasoning for effects and handlersen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record