References

Abelson and Sussman (1996)

Harold Abelson and Gerald J. Sussman. Structure and Interpretation of Computer Programs, Second Edition. MIT Press, 1996. ISBN 0-262-01153-0.

Aho et al. (2006)

Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools, 2nd edition. Addison-Wesley, 2006. ISBN 0-321-48681-1.

Appel (1992)

Andrew W. Appel. Compiling with Continuations. Cambridge University Press, 1992. ISBN 0-521-41695-7.

Appel (1998)

Andrew W. Appel. Modern Compiler Implementation in ML. Cambridge University Press, 1998. ISBN 0-521-58274-1.

Apt (1981)

Krzysztof R. Apt. Ten years of Hoare’s logic: A survey – Part 1. ACM Trans. Program. Lang. Syst., 3 (4): 431–483, 1981. doi: 10.1145/357146.357150. URL https://doi.org/10.1145/357146.357150.

Arbib and Alagic (1979)

Michael A. Arbib and Suad Alagic. Proof rules for gotos. Acta Informatica, 11: 139–148, 1979. doi: 10.1007/BF00264021. URL https://doi.org/10.1007/BF00264021.

Ariola et al. (1995)

Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. The call-by-need lambda calculus. In POPL 1995: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 233–246. ACM Press, 1995. doi: 10.1145/199448.199507. URL https://doi.org/10.1145/199448.199507.

Atkinson et al. (1978)

Russell R. Atkinson, Barbara H. Liskov, and Robert Scheifler. Aspects of implementing CLU. In Richard H. Austing, Dennis M. Conti, and Gerald L. Engel, editors, Proceedings 1978 ACM Annual Conference, Washington, DC, USA, December 4-6, 1978, Volume I, pages 123–129. ACM, 1978. doi: 10.1145/800127.804079. URL https://doi.org/10.1145/800127.804079.

Backus (1978)

John W. Backus. Can programming be liberated from the von Neumann style? A functional style and its algebra of programs. Commun. ACM, 21 (8): 613–641, 1978. doi: 10.1145/359576.359579. URL https://doi.org/10.1145/359576.359579.

Backus (1998)

John W. Backus. The history of Fortran I, II, and III. IEEE Ann. Hist. Comput., 20 (4): 68–78, 1998. doi: 10.1109/85.728232. URL https://doi.org/10.1109/85.728232.

Backus et al. (1960)

John W. Backus, Friedrich L. Bauer, Julien Green, C. Katz, John McCarthy, Alan J. Perlis, Heinz Rutishauser, Klaus Samelson, Bernard Vauquois, Joseph Henry Wegstein, Adriaan van Wijngaarden, and Michael Woodger. Report on the algorithmic language ALGOL 60. Commun. ACM, 3 (5): 299–314, 1960. doi: 10.1145/367236.367262. URL https://doi.org/10.1145/367236.367262.

Bauer (2018)

Andrej Bauer. What is algebraic about algebraic effects and handlers? CoRR, abs/1807.05923, 2018. URL http://arxiv.org/abs/1807.05923.

Bauer and Pretnar (2015)

Andrej Bauer and Matija Pretnar. Programming with algebraic effects and handlers. J. Log. Algebraic Methods Program., 84 (1): 108–123, 2015. doi: 10.1016/J.JLAMP.2014.02.001. URL https://doi.org/10.1016/j.jlamp.2014.02.001.

Böhm and Jacopini (1966)

Corrado Böhm and Giuseppe Jacopini. Flow diagrams, Turing machines and languages with only two formation rules. Commun. ACM, 9 (5): 366–371, 1966. doi: 10.1145/355592.365646. URL https://doi.org/10.1145/355592.365646.

Boruch-Gruszecki et al. (2023)

Aleksander Boruch-Gruszecki, Martin Odersky, Edward Lee, Ondrej Lhoták, and Jonathan Immanuel Brachthäuser. Capturing types. ACM Trans. Program. Lang. Syst., 45 (4): 21:1–21:52, 2023. doi: 10.1145/3618003. URL https://doi.org/10.1145/3618003.

Brachthäuser et al. (2020)

Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann. Effects as capabilities: effect handlers and lightweight effect polymorphism. Proc. ACM Program. Lang., 4 (OOPSLA): 126:1–126:30, 2020. doi: 10.1145/3428194. URL https://doi.org/10.1145/3428194.

Bruggeman et al. (1996)

Carl Bruggeman, Oscar Waddell, and R. Kent Dybvig. Representing control in the presence of one-shot continuations. In Charles N. Fischer, editor, Proceedings of the ACM SIGPLAN’96 Conference on Programming Language Design and Implementation (PLDI), Philadephia, Pennsylvania, USA, May 21-24, 1996, pages 99–107. ACM, 1996. doi: 10.1145/231379.231395. URL https://doi.org/10.1145/231379.231395.

Brumley et al. (2013)

David Brumley, JongHyup Lee, Edward J. Schwartz, and Maverick Woo. Native x86 decompilation using semantics-preserving structural analysis and iterative control-flow structuring. In Samuel T. King, editor, Proceedings of the 22th USENIX Security Symposium, Washington, DC, USA, August 14-16, 2013, pages 353–368. USENIX Association, 2013. URL https://www.usenix.org/conference/usenixsecurity13/technical-sessions/presentation/schwartz.

Butterick (2025)

Matthew Butterick. Beautiful Racket, 2025. URL https://beautifulracket.com/.

Carpenter and Doran (1977)

Brian E. Carpenter and Robert W. Doran. The other Turing machine. Comput. J., 20 (3): 269–279, 1977. doi: 10.1093/COMJNL/20.3.269. URL https://doi.org/10.1093/comjnl/20.3.269.

Clarkson et al. (2025)

Michael R. Clarkson et al. OCaml programming: Correct + efficient + beautiful, 2025. URL https://cs3110.github.io/textbook/cover.html.

Clinger et al. (1999)

William D. Clinger, Anne Hartheimer, and Eric Ost. Implementation strategies for first-class continuations. High. Order Symb. Comput., 12 (1): 7–45, 1999. doi: 10.1023/A:1010016816429. URL https://doi.org/10.1023/A:1010016816429.

Clint (1973)

Maurice Clint. Program proving: Coroutines. Acta Informatica, 2: 50–63, 1973. doi: 10.1007/BF00571463. URL https://doi.org/10.1007/BF00571463.

Clint and Hoare (1972)

Maurice Clint and C. A. R. Hoare. Program proving: Jumps and functions. Acta Informatica, 1: 214–224, 1972. doi: 10.1007/BF00288686. URL https://doi.org/10.1007/BF00288686.

Conway (1963)

Melvin E. Conway. Design of a separable transition-diagram compiler. Commun. ACM, 6 (7): 396–408, 1963. doi: 10.1145/366663.366704. URL https://doi.org/10.1145/366663.366704.

Cooper (1967)

David C. Cooper. Böhm and Jacopini’s reduction of flow charts. Commun. ACM, 10 (8): 463, 1967. doi: 10.1145/363534.363539. URL https://doi.org/10.1145/363534.363539.

Cooper and Torczon (2004)

Keith D. Cooper and Linda Torczon. Engineering a Compiler. Morgan Kaufmann, 2004. ISBN 1-55860-699-8.

Dahl et al. (1972)

Ole-Johan Dahl, Edsger W. Dijkstra, and C. A. R. Hoare. Structured programming, volume 8 of A.P.I.C. Studies in data processing. Academic Press, 1972. ISBN 978-0-12-200550-3. URL https://archive.org/details/Structured_Programming__Dahl_Dijkstra_Hoare.

Danvy and Filinski (1989)

Olivier Danvy and Andrzej Filinski. A functional abstraction of typed contexts. Technical Report DIKU 89/12, University of Copenhagen, 1989. URL https://plv.mpi-sws.org/plerg/papers/danvy-filinski-89-2up.pdf.

Danvy and Filinski (1990)

Olivier Danvy and Andrzej Filinski. Abstracting control. In LFP 1990: ACM Conference on LISP and Functional Programming, pages 151–160. ACM, 1990. doi: 10.1145/91556.91622. URL https://doi.org/10.1145/91556.91622.

Danvy and Filinski (1992)

Olivier Danvy and Andrzej Filinski. Representing control: A study of the CPS transformation. Math. Struct. Comput. Sci., 2 (4): 361–391, 1992. doi: 10.1017/S0960129500001535. URL https://doi.org/10.1017/S0960129500001535.

Danvy et al. (2007)

Olivier Danvy, Kevin Millikin, and Lasse R. Nielsen. On one-pass CPS transformations. J. Funct. Program., 17 (6): 793–812, 2007. doi: 10.1017/S0956796807006387. URL https://doi.org/10.1017/S0956796807006387.

de Bruin (1981)

Arie de Bruin. Goto statements: Semantics and deduction systems. Acta Informatica, 15: 385–424, 1981. doi: 10.1007/BF00264536. URL https://doi.org/10.1007/BF00264536.

de Moura and Ierusalimschy (2009)

Ana Lúcia de Moura and Roberto Ierusalimschy. Revisiting coroutines. ACM Trans. Program. Lang. Syst., 31 (2): 6:1–6:31, 2009. doi: 10.1145/1462166.1462167. URL https://doi.org/10.1145/1462166.1462167.

de Vilhena (2022)

Paulo Emílio de Vilhena. Proof of Programs with Effect Handlers. PhD thesis, Université Paris Cité, December 2022. URL https://theses.fr/api/v1/document/2022UNIP7133.

de Vilhena and Pottier (2021)

Paulo Emílio de Vilhena and François Pottier. A separation logic for effect handlers. Proc. ACM Program. Lang., 5 (POPL): 1–28, 2021. doi: 10.1145/3434314. URL https://doi.org/10.1145/3434314.

Delbianco and Nanevski (2013)

Germán Andrés Delbianco and Aleksandar Nanevski. Hoare-style reasoning with (algebraic) continuations. In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA - September 25 - 27, 2013, pages 363–376. ACM, 2013. doi: 10.1145/2500365.2500593. URL https://doi.org/10.1145/2500365.2500593.

Dijkstra (1968)

Edsger W. Dijkstra. Letters to the editor: go to statement considered harmful. Commun. ACM, 11 (3): 147–148, 1968. doi: 10.1145/362929.362947. URL https://doi.org/10.1145/362929.362947.

Dolan et al. (2017)

Stephen Dolan, Spiros Eliopoulos, Daniel Hillerström, Anil Madhavapeddy, K. C. Sivaramakrishnan, and Leo White. Concurrent system programming with effect handlers. In TFP 2017: Trends in Functional Programming – 18th International Symposium, volume 10788 of Lecture Notes in Computer Science, pages 98–117. Springer, 2017. doi: 10.1007/978-3-319-89719-6_6. URL https://doi.org/10.1007/978-3-319-89719-6_6.

Felleisen (1988)

Matthias Felleisen. The theory and practice of first-class prompts. In POPL 1988: Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 180–190. ACM Press, 1988. doi: 10.1145/73560.73576. URL https://doi.org/10.1145/73560.73576.

Floyd (1967)

Robert W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, Proceedings of Symposium on Applied Mathematics, volume 19, pages 19–32. American Mathematical Society, 1967. ISBN 0821867288.

Friedman (1988)

Daniel P. Friedman. Applications of continuations. Invited tutorial, Fifteenth Annual ACM Symposium on Principles of Programming Languages, 1988. URL http://www.cs.indiana.edu/hyplan/dfried/appcont.pdf.

Friedman and Wand (2008)

Daniel P. Friedman and Mitchell Wand. Essentials of programming languages (3. ed.). MIT Press, 2008. ISBN 978-0-262-06279-4.

Garrigue (2004)

Jacques Garrigue. Relaxing the value restriction. In FLOPS 2004: Functional and Logic Programming, 7th International Symposium, volume 2998 of Lecture Notes in Computer Science, pages 196–213. Springer, 2004. doi: 10.1007/978-3-540-24754-8_15. URL https://doi.org/10.1007/978-3-540-24754-8_15.

Gasbichler and Sperber (2002)

Martin Gasbichler and Michael Sperber. Final shift for call/cc: : direct implementation of shift and reset. In Mitchell Wand and Simon L. Peyton Jones, editors, Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002, pages 271–282. ACM, 2002. doi: 10.1145/581478.581504. URL https://doi.org/10.1145/581478.581504.

Goodenough (1975)

John B. Goodenough. Exception handling: Issues and a proposed notation. Commun. ACM, 18 (12): 683–696, 1975. doi: 10.1145/361227.361230. URL https://doi.org/10.1145/361227.361230.

Griswold (1988)

Ralph E. Griswold. Programming with generators. Comput. J., 31 (3): 220–228, 1988. doi: 10.1093/COMJNL/31.3.220. URL https://doi.org/10.1093/comjnl/31.3.220.

Gunter et al. (1995)

Carl A. Gunter, Didier Rémy, and Jon G. Riecke. A generalization of exceptions and control in ML-like languages. In FPCA 1995: 7th International Conference on Functional Programming Languages and Computer Architecture, pages 12–23. ACM, 1995. doi: 10.1145/224164.224173. URL https://doi.org/10.1145/224164.224173.

Harel (1980)

David Harel. On folk theorems. Commun. ACM, 23 (7): 379–389, 1980. doi: 10.1145/358886.358892. URL https://doi.org/10.1145/358886.358892.

Harper (2016)

Robert Harper. Practical Foundations for Programming Languages (2nd. Ed.). Cambridge University Press, 2016. ISBN 9781107150300. URL https://www.cs.cmu.edu/~rwh/pfpl/index.html.

Harper and Lillibridge (1993)

Robert Harper and Mark Lillibridge. Polymorphic type assignment and CPS conversion. LISP Symb. Comput., 6 (3-4): 361–380, 1993. doi: 10.1007/BF01019463.

Henglein et al. (2005)

Fritz Henglein, Henning Makholm, and Henning Niss. Effect types and region-based memory management. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, pages 102–135. The MIT Press, 2005. ISBN 0-262-16228-8. doi: 10.7551/mitpress/1104.003.0005.

Hillerström and Lindley (2016)

Daniel Hillerström and Sam Lindley. Liberating effects with rows and handlers. In James Chapman and Wouter Swierstra, editors, TyDe@ICFP 2016: 1st International Workshop on Type-Driven Development, pages 15–27. ACM, 2016. doi: 10.1145/2976022.2976033. URL https://doi.org/10.1145/2976022.2976033.

Hillerström et al. (2020)

Daniel Hillerström, Sam Lindley, and Robert Atkey. Effect handlers via generalised continuations. J. Funct. Program., 30: e5, 2020. doi: 10.1017/S0956796820000040. URL https://doi.org/10.1017/S0956796820000040.

Hillerström (2021)

Daniel Hillerström. Foundations for Programming and Implementing Effect Handlers. PhD thesis, The University of Edinburgh, 2021.

Hoare (1969)

C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12 (10): 576–580, 1969. doi: 10.1145/363235.363259. URL https://doi.org/10.1145/363235.363259.

Hughes (2000)

John Hughes. Generalising monads to arrows. Sci. Comput. Program., 37 (1-3): 67–111, 2000. doi: 10.1016/S0167-6423(99)00023-4. URL https://doi.org/10.1016/S0167-6423(99)00023-4.

Johnson and Foote (1988)

R. E. Johnson and B. Foote. Designing reusable classes. Journal of Object-Oriented Programming, 1 (2): 22–35, 1988. URL https://www.laputan.org/drc/drc.html.

Jung et al. (2018)

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program., 28: e20, 2018. doi: 10.1017/S0956796818000151. URL https://doi.org/10.1017/S0956796818000151.

Kennedy (2007)

Andrew Kennedy. Compiling with continuations, continued. In Ralf Hinze and Norman Ramsey, editors, Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, October 1-3, 2007, pages 177–190. ACM, 2007. doi: 10.1145/1291151.1291179. URL https://doi.org/10.1145/1291151.1291179.

Kiselyov (2012)

Oleg Kiselyov. Delimited control in OCaml, abstractly and concretely. Theor. Comput. Sci., 435: 56–76, 2012. doi: 10.1016/J.TCS.2012.02.025. URL https://doi.org/10.1016/j.tcs.2012.02.025.

Kiselyov and Ishii (2015)

Oleg Kiselyov and Hiromi Ishii. Freer monads, more extensible effects. In Ben Lippmeier, editor, Haskell 2015: 8th ACM SIGPLAN Symposium on Haskell, pages 94–105. ACM, 2015. doi: 10.1145/2804302.2804319. URL https://doi.org/10.1145/2804302.2804319.

Knuth (1974)

Donald E. Knuth. Structured programming with go to statements. ACM Comput. Surv., 6 (4): 261–301, 1974. doi: 10.1145/356635.356640. URL https://doi.org/10.1145/356635.356640.

Kosaraju (1974)

S. Rao Kosaraju. Analysis of structured programs. J. Comput. Syst. Sci., 9 (3): 232–255, 1974. doi: 10.1016/S0022-0000(74)80043-7. URL https://doi.org/10.1016/S0022-0000(74)80043-7.

Landin (1964)

P. J. Landin. The mechanical evaluation of expressions. Comput. J., 6 (4): 308–320, 1964. doi: 10.1093/COMJNL/6.4.308. URL https://doi.org/10.1093/comjnl/6.4.308.

Landin (1965)

P. J. Landin. Correspondence between ALGOL 60 and Church’s lambda-notation: part I. Commun. ACM, 8 (2): 89–101, 1965. doi: 10.1145/363744.363749. URL https://doi.org/10.1145/363744.363749.

Landin (1966)

P. J. Landin. The next 700 programming languages. Commun. ACM, 9 (3): 157–166, 1966. doi: 10.1145/365230.365257. URL https://doi.org/10.1145/365230.365257.

Leijen (2014)

Daan Leijen. Koka: Programming with row polymorphic effect types. In Paul Blain Levy and Neel Krishnaswami, editors, Proceedings 5th Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2014, Grenoble, France, 12 April 2014, volume 153 of EPTCS, pages 100–126, 2014. doi: 10.4204/EPTCS.153.8. URL https://doi.org/10.4204/EPTCS.153.8.

Leijen (2017)

Daan Leijen. Type directed compilation of row-typed algebraic effects. In POPL 2017: 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pages 486–499. ACM, 2017. doi: 10.1145/3009837.3009872. URL https://doi.org/10.1145/3009837.3009872.

Liskov and Snyder (1979)

Barbara H. Liskov and Alan Snyder. Exception handling in CLU. IEEE Trans. Software Eng., 5 (6): 546–558, 1979. doi: 10.1109/TSE.1979.230191. URL https://doi.org/10.1109/TSE.1979.230191.

Lucassen and Gifford (1988)

John M. Lucassen and David K. Gifford. Polymorphic effect systems. In POPL 1988: 15th Annual ACM Symposium on Principles of Programming Languages, pages 47–57. ACM Press, 1988. doi: 10.1145/73560.73564. URL https://doi.org/10.1145/73560.73564.

Materzok and Biernacki (2011)

Marek Materzok and Dariusz Biernacki. Subtyping delimited continuations. In ICFP 2011: 16th ACM SIGPLAN international conference on Functional Programming, pages 81–93. ACM, 2011. doi: 10.1145/2034773.2034786. URL https://doi.org/10.1145/2034773.2034786.

McBride and Paterson (2008)

Conor McBride and Ross Paterson. Applicative programming with effects. J. Funct. Program., 18 (1): 1–13, 2008. doi: 10.1017/S0956796807006326. URL https://doi.org/10.1017/S0956796807006326.

McCarthy (1960)

John McCarthy. Recursive functions of symbolic expressions and their computation by machine, part I. Commun. ACM, 3 (4): 184–195, 1960. doi: 10.1145/367177.367199. URL https://doi.org/10.1145/367177.367199.

Milner (1978)

Robin Milner. A theory of type polymorphism in programming. J. Comput. Syst. Sci., 17 (3): 348–375, 1978. doi: 10.1016/0022-0000(78)90014-4. URL https://doi.org/10.1016/0022-0000(78)90014-4.

Moggi (1989)

Eugenio Moggi. Computational lambda-calculus and monads. In LICS 1989: Fourth Annual Symposium on Logic in Computer Science, pages 14–23. IEEE Computer Society, 1989. doi: 10.1109/LICS.1989.39155. URL https://doi.org/10.1109/LICS.1989.39155.

Moggi (1991)

Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93 (1): 55–92, 1991. doi: 10.1016/0890-5401(91)90052-4. URL https://doi.org/10.1016/0890-5401(91)90052-4.

Monperrus et al. (2014)

Martin Monperrus, Maxence Germain de Montauzan, Benoit Cornu, Raphael Marvie, and Romain Rouvoy. Challenging analytical knowledge on exception-handling: An empirical study of 32 Java software packages. Technical Report hal-01093908, Laboratoire d’Informatique Fondamentale de Lille, 2014. URL https://hal.science/hal-01093908.

Morris and Jones (1984)

F. Lockwood Morris and Cliff B. Jones. An early program proof by Alan Turing. IEEE Ann. Hist. Comput., 6 (2): 139–143, 1984. doi: 10.1109/MAHC.1984.10017. URL https://doi.org/10.1109/MAHC.1984.10017.

Newbern et al. (2025)

Jeff Newbern et al. All about monads. In Haskell Wiki. 2025. URL https://wiki.haskell.org/All_About_Monads.

Nielson et al. (1999)

Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of program analysis. Springer, 1999. ISBN 978-3-540-65410-0. doi: 10.1007/978-3-662-03811-6. URL https://doi.org/10.1007/978-3-662-03811-6.

Nielson and Nielson (2007)

Hanne Riis Nielson and Flemming Nielson. Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science. Springer, 2007. ISBN 978-1-84628-691-9. doi: 10.1007/978-1-84628-692-6. URL https://doi.org/10.1007/978-1-84628-692-6.

Odersky et al. (2021)

Martin Odersky, Aleksander Boruch-Gruszecki, Jonathan Immanuel Brachthäuser, Edward Lee, and Ondrej Lhoták. Safer exceptions for scala. In SCALA 2021: 12th ACM SIGPLAN International Symposium on Scala, pages 1–11. ACM, 2021. doi: 10.1145/3486610.3486893. URL https://doi.org/10.1145/3486610.3486893.

O’Donnell (1982)

Michael J. O’Donnell. A critique of the foundations of Hoare style programming logics. Commun. ACM, 25 (12): 927–935, 1982. doi: 10.1145/358728.358748. URL https://doi.org/10.1145/358728.358748.

O’Hearn (2007)

Peter W. O’Hearn. Resources, concurrency, and local reasoning. Theor. Comput. Sci., 375 (1-3): 271–307, 2007. doi: 10.1016/J.TCS.2006.12.035. URL https://doi.org/10.1016/j.tcs.2006.12.035.

O’Hearn (2019)

Peter W. O’Hearn. Separation logic. Commun. ACM, 62 (2): 86–95, 2019. doi: 10.1145/3211968. URL https://doi.org/10.1145/3211968.

Padua (2000)

David A. Padua. The Fortran I compiler. Comput. Sci. Eng., 2 (1): 70–75, 2000. doi: 10.1109/5992.814661. URL https://doi.org/10.1109/5992.814661.

Parkinson et al. (2006)

Matthew J. Parkinson, Richard Bornat, and Cristiano Calcagno. Variables as resource in Hoare logics. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 137–146. IEEE Computer Society, 2006. doi: 10.1109/LICS.2006.52. URL https://doi.org/10.1109/LICS.2006.52.

Peterson et al. (1973)

W. Wesley Peterson, Tadao Kasami, and Nobuki Tokura. On the capabilities of while, repeat, and exit statements. Commun. ACM, 16 (8): 503–512, 1973. doi: 10.1145/355609.362337. URL https://doi.org/10.1145/355609.362337.

Peyton Jones (1987)

Simon L. Peyton Jones. The Implementation of Functional Programming Languages. Prentice-Hall, 1987. ISBN 978-0-13-453333-9. URL https://simon.peytonjones.org/slpj-book-1987/.

Pierce (2002)

Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. ISBN 978-0-262-16209-8.

Pierce et al. (2025)

Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent Yorgey. Programming Language Foundations, volume 2 of Software Foundations. 2025. URL https://softwarefoundations.cis.upenn.edu/.

Plotkin (1975)

Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci., 1 (2): 125–159, 1975. doi: 10.1016/0304-3975(75)90017-1. URL https://doi.org/10.1016/0304-3975(75)90017-1.

Plotkin and Power (2003)

Gordon D. Plotkin and John Power. Algebraic operations and generic effects. Appl. Categorical Struct., 11 (1): 69–94, 2003. doi: 10.1023/A:1023064908962. URL https://doi.org/10.1023/A:1023064908962.

Plotkin and Power (2008)

Gordon D. Plotkin and John Power. Tensors of comodels and models for operational semantics. In MFPS 2008: 24th Conference on the Mathematical Foundations of Programming Semantics, volume 218 of Electronic Notes in Theoretical Computer Science, pages 295–311. Elsevier, 2008. doi: 10.1016/J.ENTCS.2008.10.018. URL https://doi.org/10.1016/j.entcs.2008.10.018.

Plotkin and Pretnar (2013)

Gordon D. Plotkin and Matija Pretnar. Handling algebraic effects. Log. Methods Comput. Sci., 9 (4), 2013. doi: 10.2168/LMCS-9(4:23)2013. URL https://doi.org/10.2168/LMCS-9(4:23)2013.

Pottier and Rémy (2005)

François Pottier and Didier Rémy. The essence of ML type inference. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, pages 404–489. The MIT Press, 2005. ISBN 0-262-16228-8. doi: 10.7551/mitpress/1104.003.0016.

Pratt and Zelkowitz (2000)

Terrence W. Pratt and Marvin V. Zelkowitz. Programming Languages: Design and Implementation. Prentice Hall, 4th ed. edition, 2000. ISBN 0130291048.

Pretnar (2015)

Matija Pretnar. An introduction to algebraic effects and handlers. invited tutorial paper. In MFPS 2015: 31st Conference on the Mathematical Foundations of Programming Semantics, volume 319 of Electronic Notes in Theoretical Computer Science, pages 19–35. Elsevier, 2015. doi: 10.1016/J.ENTCS.2015.12.003. URL https://doi.org/10.1016/j.entcs.2015.12.003.

Ramsey (2022)

Norman Ramsey. Beyond Relooper: recursive translation of unstructured control flow to structured control flow (functional pearl). Proc. ACM Program. Lang., 6 (ICFP): 1–22, 2022. doi: 10.1145/3547621. URL https://doi.org/10.1145/3547621.

Ramshaw (1988)

Lyle Ramshaw. Eliminating go to’s while preserving program structure. J. ACM, 35 (4): 893–920, 1988. doi: 10.1145/48014.48021. URL https://doi.org/10.1145/48014.48021.

Rémy (1989)

Didier Rémy. Typechecking records and variants in a natural extension of ML. In POPL 1989: 16th Annual ACM Symposium on Principles of Programming Languages, pages 77–88. ACM Press, 1989. doi: 10.1145/75277.75284. URL https://doi.org/10.1145/75277.75284.

Reynolds (1993)

John C. Reynolds. The discoveries of continuations. LISP Symb. Comput., 6 (3-4): 233–248, 1993. doi: 10.1007/BF01019459.

Reynolds (1998)

John C. Reynolds. Definitional interpreters for higher-order programming languages. High. Order Symb. Comput., 11 (4): 363–397, 1998. doi: 10.1023/A:1010027404223. URL https://doi.org/10.1023/A:1010027404223.

Reynolds (2002)

John C. Reynolds. Separation logic: A logic for shared mutable data structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pages 55–74. IEEE Computer Society, 2002. doi: 10.1109/LICS.2002.1029817. URL https://doi.org/10.1109/LICS.2002.1029817.

Rutishauser (1967)

Heinz Rutishauser. Handbook for Automatic Computation: Description of Algol 60. Springer, 1967. ISBN 978-3-662-37359-0. URL https://algol60.org/docs/Rutishauser_Description_of_ALGOL_60_1967.pdf.

Schemenauer et al. (2001)

Neil Schemenauer, Tim Peters, and Magnus Lie Hetland. Pep 255 — simple generators. Python Extension Proposal 255, 2001. URL https://peps.python.org/pep-0255.

Scott and Aldrich (2025)

Michael L. Scott and Jonathan Aldrich. Programming Language Pragmatics. Morgan Kaufmann, 5th ed. edition, 2025. ISBN 978-0323999663.

Sivaramakrishnan et al. (2021)

KC Sivaramakrishnan, Stephen Dolan, Leo White, Tom Kelly, Sadiq Jaffer, and Anil Madhavapeddy. Retrofitting effect handlers onto OCaml. In PLDI 2021: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pages 206–221. ACM, 2021. doi: 10.1145/3453483.3454039. URL https://doi.org/10.1145/3453483.3454039.

Speed (2000)

Richard Speed. ALGOL 60 at 60: The greatest computer language you’ve never used and grandaddy of the programming family tree. The Register, May 2000. URL https://www.theregister.com/2020/05/15/algol_60_at_60/.

Steele (1978)

Guy L. Steele, Jr. RABBIT: A compiler for SCHEME. Technical Report AITR 474, MIT, 1978. URL https://dspace.mit.edu/handle/1721.1/6913.

Stroustrup (2019)

Bjarne Stroustrup. C++ exceptions and alternatives. Technical Report P1947, ISO IEC JTC1/SC22/WG21 C++ Standards Committee, 2019. URL https://wg21.link/p1947.

Sussman and Steele (1975)

Gerald J. Sussman and Guy L. Steele, Jr. SCHEME: An interpreter for extended lambda calculus. Technical Report AIM 349, MIT, 1975. URL http://hdl.handle.net/1721.1/5794.

Swamy et al. (2016)

Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella-Béguelin. Dependent types and multi-monadic effects in F*. In POPL 2016: 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 256–270. ACM, 2016. doi: 10.1145/2837614.2837655. URL https://doi.org/10.1145/2837614.2837655.

Talpin and Jouvelot (1994)

Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. Inf. Comput., 111 (2): 245–296, 1994. doi: 10.1006/INCO.1994.1046. URL https://doi.org/10.1006/inco.1994.1046.

Thielecke (1998)

Hayo Thielecke. An introduction to landin’s “a generalization of jumps and labels”. High. Order Symb. Comput., 11 (2): 117–123, 1998. doi: 10.1023/A:1010060315625. URL https://doi.org/10.1023/A:1010060315625.

Timany and Birkedal (2019)

Amin Timany and Lars Birkedal. Mechanized relational verification of concurrent programs with continuations. Proc. ACM Program. Lang., 3 (ICFP): 105:1–105:28, 2019. doi: 10.1145/3341709. URL https://doi.org/10.1145/3341709.

Turing (1946)

Alan Turing. Proposals for development in the mathematics dvision of an automatic computing engine (ACE). Technical Report E.882, National Physical Laboratory, March 1946. URL https://turingarchive.kings.cam.ac.uk/unpublished-manuscripts-and-drafts-amtc/amt-c-32.

Turing (1949)

Alan Turing. Checking a large routine. In Report of a Conference on High Speed Automatic Calculating Machines, pages 67–69. Cambridge University, June 1949. URL https://turingarchive.kings.cam.ac.uk/publications-lectures-and-talks-amtb/amt-b-8. Reprinted, corrected and commented in Morris and Jones (1984).

Uustalu and Vene (2008)

Tarmo Uustalu and Varmo Vene. Comonadic notions of computation. In CMCS 2008: 9th Workshop on Coalgebraic Methods in Computer Science, volume 203 of Electronic Notes in Theoretical Computer Science, pages 263–284. Elsevier, 2008. doi: 10.1016/J.ENTCS.2008.05.029. URL https://doi.org/10.1016/j.entcs.2008.05.029.

van Rooij and Krebbers (2025)

Orpheas van Rooij and Robbert Krebbers. Affect: An affine type and effect system. Proc. ACM Program. Lang., 9 (POPL): 126–154, 2025. doi: 10.1145/3704841. URL https://doi.org/10.1145/3704841.

Van Roy and Haridi (2004)

Peter Van Roy and Seif Haridi. Concepts, Techniques, and Models of Computer Programming. MIT Press, 2004. ISBN 0-262-22069-5. URL http://www.info.ucl.ac.be/people/PVR/book.html.

von Neumann (1945)

John von Neumann. First draft of a report on the EDVAC. Technical report, University of Pennsylvania, Moore School of Electrical Engineering, June 1945. URL https://archive.computerhistory.org/resources/text/Knuth_Don_X4100/PDF_index/k-8-pdf/k-8-u2593-Draft-EDVAC.pdf.

Vouillon (2008)

Jérôme Vouillon. Lwt: a cooperative thread library. In Eijiro Sumii, editor, Proceedings of the ACM Workshop on ML, 2008, Victoria, BC, Canada, September 21, 2008, pages 3–12. ACM, 2008. doi: 10.1145/1411304.1411307. URL https://doi.org/10.1145/1411304.1411307.

Wadler (1992)

Philip Wadler. The essence of functional programming. In Ravi Sethi, editor, POPL 1992: 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 1–14. ACM Press, 1992. doi: 10.1145/143165.143169. URL https://doi.org/10.1145/143165.143169.

Wadler (1995)

Philip Wadler. Monads for functional programming. In AFP 1995: 1st International Spring School on Advanced Functional Programming Techniques, volume 925 of Lecture Notes in Computer Science, pages 24–52. Springer, 1995. doi: 10.1007/3-540-59451-5_2. URL https://doi.org/10.1007/3-540-59451-5_2.

Wadler and Thiemann (2003)

Philip Wadler and Peter Thiemann. The marriage of effects and monads. ACM Trans. Comput. Log., 4 (1): 1–32, 2003. doi: 10.1145/601775.601776. URL https://doi.org/10.1145/601775.601776.

Wand (1987)

Mitchell Wand. Complete type inference for simple objects. In LICS 1987: Symposium on Logic in Computer Science, pages 37–44. IEEE Computer Society, 1987. URL http://www.ccs.neu.edu/home/wand/papers/wand-lics-87.pdf.

Winskel (1993)

Glynn Winskel. The formal semantics of programming languages - an introduction. Foundation of computing series. MIT Press, 1993. ISBN 978-0-262-23169-5.

Wright and Felleisen (1994)

Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Inf. Comput., 115 (1): 38–94, 1994. doi: 10.1006/INCO.1994.1093. URL https://doi.org/10.1006/inco.1994.1093.

Xia et al. (2020)

Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang., 4 (POPL): 51:1–51:32, 2020. doi: 10.1145/3371119. URL https://doi.org/10.1145/3371119.

Xie and Leijen (2021)

Ningning Xie and Daan Leijen. Generalized evidence passing for effect handlers: efficient compilation of effect handlers to C. Proc. ACM Program. Lang., 5 (ICFP): 1–30, 2021. doi: 10.1145/3473576. URL https://doi.org/10.1145/3473576.

Yakdan et al. (2015)

Khaled Yakdan, Sebastian Eschweiler, Elmar Gerhards-Padilla, and Matthew Smith. No more gotos: Decompilation using pattern-independent control-flow structuring and semantic-preserving transformations. In 22nd Annual Network and Distributed System Security Symposium, NDSS 2015, San Diego, California, USA, February 8-11, 2015. The Internet Society, 2015. URL https://www.ndss-symposium.org/ndss2015/no-more-gotos-decompilation-using-pattern-independent-control-flow-structuring-and-semantics.

Yang et al. (2022)

Zhixuan Yang, Marco Paviotti, Nicolas Wu, Birthe van den Berg, and Tom Schrijvers. Structured handling of scoped effects. In ESOP 2022: Programming Languages and Systems - 31st European Symposium on Programming, volume 13240 of Lecture Notes in Computer Science, pages 462–491. Springer, 2022. doi: 10.1007/978-3-030-99336-8_17. URL https://doi.org/10.1007/978-3-030-99336-8_17.