references.bib

@article{bauer2015programming,
  title={Programming with algebraic effects and handlers},
  author={Bauer, Andrej and Pretnar, Matija},
  journal={Journal of logical and algebraic methods in programming},
  volume={84},
  number={1},
  pages={108--123},
  year={2015},
  publisher={Elsevier}
}

@article{bauer-pretnar-2014,
	title = {An {Effect} {System} for {Algebraic} {Effects} and {Handlers}},
	volume = {Volume 10, Issue 4},
	issn = {1860-5974},
	url = {https://lmcs.episciences.org/1153},
	doi = {10.2168/LMCS-10(4:9)2014},
	abstract = {We present an effect system for core Eff, a simplified variant of Eff , which is an ML-style programming language with first-class algebraic effects and handlers. We define an expressive effect system and prove safety of operational semantics with respect to it. Then we give a domain-theoretic denotational semantics of core Eff , using Pitts’s theory of minimal invariant relations, and prove it adequate. We use this fact to develop tools for finding useful contextual equivalences, including an induction principle. To demonstrate their usefulness, we use these tools to derive the usual equations for mutable state, including a general commutativity law for computations using non-interfering references. We have formalized the effect system, the operational semantics, and the safety theorem in Twelf.},
	language = {en},
	urldate = {2023-04-27},
	journal = {Logical Methods in Computer Science},
	author = {Bauer, Andrej and Pretnar, Matija},
	month = dec,
	year = {2014},
	pages = {1153},
}

@inproceedings{siek2015,
  author    = {Jeremy G. Siek and
               Michael M. Vitousek and
               Matteo Cimini and
               John Tang Boyland},
  editor    = {Thomas Ball and
               Rastislav Bod{\'{\i}}k and
               Shriram Krishnamurthi and
               Benjamin S. Lerner and
               Greg Morrisett},
  title     = {Refined Criteria for Gradual Typing},
  booktitle = {1st Summit on Advances in Programming Languages, {SNAPL} 2015, May
               3-6, 2015, Asilomar, California, {USA}},
  series    = {LIPIcs},
  volume    = {32},
  pages     = {274--293},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2015},
  url       = {https://doi.org/10.4230/LIPIcs.SNAPL.2015.274},
  doi       = {10.4230/LIPIcs.SNAPL.2015.274},
  timestamp = {Tue, 11 Feb 2020 15:52:14 +0100},
  biburl    = {https://dblp.org/rec/conf/snapl/SiekVCB15.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{castagna2019,
  title={Gradual typing: a new perspective},
  author={Castagna, Giuseppe and Lanvin, Victor and Petrucciani, Tommaso and Siek, Jeremy G},
  journal={Proceedings of the ACM on Programming Languages},
  volume={3},
  number={POPL},
  pages={1--32},
  year={2019},
  publisher={ACM New York, NY, USA}
}

@article{sekiyama2019gradual,
  title={Gradual Typing for Extensibility by Rows},
  author={Sekiyama, Taro and Igarashi, Atsushi},
  journal={arXiv preprint arXiv:1910.08480},
  year={2019}
}

@article{schwerter-2016,
  title={Gradual type-and-effect systems},
  author={Schwerter, Felipe Ba{\~n}ados and Garcia, Ronald and Tanter, {\'E}ric},
  journal={Journal of functional programming},
  volume={26},
  year={2016},
  publisher={Cambridge University Press}
}

@article{mcbride2000,
  title={Dependently typed functional programs and their proofs},
  author={McBride, Conor},
  year={2000},
  publisher={University of Edinburgh. College of Science and Engineering. School of~…}
}

@article{boyland2014problem,
  title={The problem of structural type tests in a gradual-typed language},
  author={Boyland, John Tang},
  journal={Foundations of Object-Oriented Langauges},
  year={2014}
}

@article{plotkin-power-2001,
  title={Semantics for algebraic operations},
  author={Plotkin, Gordon and Power, John},
  journal={Electronic Notes in Theoretical Computer Science},
  volume={45},
  pages={332--345},
  year={2001},
  publisher={Elsevier}
}

@inproceedings{plotkin-pretnar-2009,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Handlers of {Algebraic} {Effects}},
	isbn = {978-3-642-00590-9},
	doi = {10.1007/978-3-642-00590-9_7},
	abstract = {We present an algebraic treatment of exception handlers and, more generally, introduce handlers for other computational effects representable by an algebraic theory. These include nondeterminism, interactive input/output, concurrency, state, time, and their combinations; in all cases the computation monad is the free-model monad of the theory. Each such handler corresponds to a model of the theory for the effects at hand. The handling construct, which applies a handler to a computation, is based on the one introduced by Benton and Kennedy, and is interpreted using the homomorphism induced by the universal property of the free model. This general construct can be used to describe previously unrelated concepts from both theory and practice.},
	language = {en},
	booktitle = {Programming {Languages} and {Systems}},
	publisher = {Springer},
	author = {Plotkin, Gordon and Pretnar, Matija},
	editor = {Castagna, Giuseppe},
	year = {2009},
	keywords = {Algebraic Theory, Base Signature, Base Type, Function Symbol, Relation Symbol},
	pages = {80--94},
}

@inproceedings{siek-taha-2006,
author = {Siek, Jeremy and Taha, Walid},
year = {2006},
month = {01},
pages = {},
title = {Gradual typing for functional languages},
journal = {Scheme and Functional Programming}
}

@article{new-ahmed-2018,
	title = {Graduality from embedding-projection pairs},
	volume = {2},
	issn = {2475-1421},
	url = {https://dl.acm.org/doi/10.1145/3236768},
	doi = {10.1145/3236768},
	language = {en},
	number = {ICFP},
	urldate = {2023-04-27},
	journal = {Proceedings of the ACM on Programming Languages},
	author = {New, Max S. and Ahmed, Amal},
	month = jul,
	year = {2018},
	pages = {1--30},
}

@inproceedings{marino-2009,
	address = {Savannah GA USA},
	title = {A generic type-and-effect system},
	isbn = {978-1-60558-420-1},
	url = {https://dl.acm.org/doi/10.1145/1481861.1481868},
	doi = {10.1145/1481861.1481868},
	abstract = {Type-and-effect systems are a natural approach for statically reasoning about a program’s execution. They have been used to track a variety of computational effects, for example memory manipulation, exceptions, and locking. However, each type-and-effect system is typically implemented as its own monolithic type system that hard-codes a particular syntax of effects along with particular rules to track and control those effects.},
	language = {en},
	urldate = {2023-04-27},
	booktitle = {Proceedings of the 4th international workshop on {Types} in language design and implementation},
	publisher = {ACM},
	author = {Marino, Daniel and Millstein, Todd},
	month = jan,
	year = {2009},
	pages = {39--50},
}

@inproceedings{dolan-2015,
  title={Effective concurrency through algebraic effects},
  author={Dolan, Stephen and White, Leo and Sivaramakrishnan, KC and Yallop, Jeremy and Madhavapeddy, Anil},
  booktitle={OCaml Workshop},
  volume={13},
  year={2015}
}

@article{ghc-delcont,
  author={King, Alexis},
  month={January},
  year={2021},
  title={Delimited continuations primops},
  journal={GHC Proposals},
  url={https://github.com/ghc-proposals/ghc-proposals/blob/310b91eb3129b06e629dabfe302513c5fbcbd30f/proposals/0313-delimited-continuation-primops.rst}
}

@misc{wasmfx,
  author={Lindley, Sam and Hillerström, Daniel and Rossberg, Andreas},
  year={2022},
  title={Effect Handlers for WebAssembly},
  url={https://wasmfx.dev/}
}

@article{kammar2013handlers,
  title={Handlers in action},
  author={Kammar, Ohad and Lindley, Sam and Oury, Nicolas},
  journal={ACM SIGPLAN Notices},
  volume={48},
  number={9},
  pages={145--158},
  year={2013},
  publisher={ACM New York, NY, USA}
}

@inproceedings{leijen04,
  author       = {Daan Leijen},
  editor       = {Paul Blain Levy and
                  Neel Krishnaswami},
  title        = {Koka: Programming with Row Polymorphic Effect Types},
  booktitle    = {Proceedings 5th Workshop on Mathematically Structured Functional Programming,
                  MSFP@ETAPS 2014, Grenoble, France, 12 April 2014},
  series       = {{EPTCS}},
  volume       = {153},
  pages        = {100--126},
  year         = {2014},
  url          = {https://doi.org/10.4204/EPTCS.153.8},
  doi          = {10.4204/EPTCS.153.8},
  timestamp    = {Wed, 29 Sep 2021 08:56:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/Leijen14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{dobedo,
  author       = {Sam Lindley and
                  Conor McBride and
                  Craig McLaughlin},
  editor       = {Giuseppe Castagna and
                  Andrew D. Gordon},
  title        = {Do be do be do},
  booktitle    = {Proceedings of the 44th {ACM} {SIGPLAN} Symposium on Principles of
                  Programming Languages, {POPL} 2017, Paris, France, January 18-20,
                  2017},
  pages        = {500--514},
  publisher    = {{ACM}},
  year         = {2017},
  url          = {https://doi.org/10.1145/3009837.3009897},
  doi          = {10.1145/3009837.3009897},
  timestamp    = {Mon, 14 Feb 2022 09:20:26 +0100},
  biburl       = {https://dblp.org/rec/conf/popl/LindleyMM17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{hillerstrom2016,
  title={Compiling Links effect handlers to the OCaml backend},
  author={Hillerstr{\"o}m, Daniel and Lindley, Sam and Sivaramakrishnan, K},
  booktitle={ML Workshop},
  volume={116},
  year={2016}
}

@article{greff-2023,
  author       = {Max S. New and
                  Eric Giovannini and
                  Daniel R. Licata},
  title        = {Gradual Typing for Effect Handlers},
  journal      = {CoRR},
  volume       = {abs/2304.02145},
  year         = {2023},
  url          = {https://doi.org/10.48550/arXiv.2304.02145},
  doi          = {10.48550/arXiv.2304.02145},
  eprinttype    = {arXiv},
  eprint       = {2304.02145},
  timestamp    = {Mon, 17 Apr 2023 15:20:10 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2304-02145.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}