refs.bib

@inproceedings{fscd19,
  author    = {Maciej Pir{\'{o}}g and
               Piotr Polesiuk and
               Filip Sieczkowski},
  editor    = {Herman Geuvers},
  title     = {Typed Equivalence of Effect Handlers and Delimited Control},
  booktitle = {4th International Conference on Formal Structures for Computation
               and Deduction, {FSCD} 2019, June 24-30, 2019, Dortmund, Germany},
  series    = {LIPIcs},
  volume    = {131},
  pages     = {30:1--30:16},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2019},
  url       = {https://doi.org/10.4230/LIPIcs.FSCD.2019.30},
  doi       = {10.4230/LIPIcs.FSCD.2019.30},
  timestamp = {Thu, 14 Oct 2021 10:42:37 +0200},
  biburl    = {https://dblp.org/rec/conf/rta/PirogPS19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{hwc,
  author    = {Dariusz Biernacki and
               Maciej Pir{\'{o}}g and
               Piotr Polesiuk and
               Filip Sieczkowski},
  title     = {Handle with care: relational interpretation of algebraic effects and
               handlers},
  journal   = {Proc. {ACM} Program. Lang.},
  volume    = {2},
  number    = {{POPL}},
  pages     = {8:1--8:30},
  year      = {2018},
  url       = {https://doi.org/10.1145/3158096},
  doi       = {10.1145/3158096},
  timestamp = {Thu, 14 Oct 2021 08:48:51 +0200},
  biburl    = {https://dblp.org/rec/journals/pacmpl/BiernackiPPS18.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{marriage,
  author    = {Chung{-}Kil Hur and
               Derek Dreyer and
               Georg Neis and
               Viktor Vafeiadis},
  editor    = {John Field and
               Michael Hicks},
  title     = {The marriage of bisimulations and Kripke logical relations},
  booktitle = {Proceedings of the 39th {ACM} {SIGPLAN-SIGACT} Symposium on Principles
               of Programming Languages, {POPL} 2012, Philadelphia, Pennsylvania,
               USA, January 22-28, 2012},
  pages     = {59--72},
  publisher = {{ACM}},
  year      = {2012},
  url       = {https://doi.org/10.1145/2103656.2103666},
  doi       = {10.1145/2103656.2103666},
  timestamp = {Thu, 24 Jun 2021 16:19:31 +0200},
  biburl    = {https://dblp.org/rec/conf/popl/HurDNV12.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{hia,
  author    = {Ohad Kammar and
               Sam Lindley and
               Nicolas Oury},
  editor    = {Greg Morrisett and
               Tarmo Uustalu},
  title     = {Handlers in action},
  booktitle = {{ACM} {SIGPLAN} International Conference on Functional Programming,
               ICFP'13, Boston, MA, {USA} - September 25 - 27, 2013},
  pages     = {145--158},
  publisher = {{ACM}},
  year      = {2013},
  url       = {https://doi.org/10.1145/2500365.2500590},
  doi       = {10.1145/2500365.2500590},
  timestamp = {Thu, 24 Jun 2021 16:19:30 +0200},
  biburl    = {https://dblp.org/rec/conf/icfp/KammarLO13.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{exrw,
  author    = {Sam Lindley},
  editor    = {Simona Ronchi Della Rocca},
  title     = {Extensional Rewriting with Sums},
  booktitle = {Typed Lambda Calculi and Applications, 8th International Conference,
               {TLCA} 2007, Paris, France, June 26-28, 2007, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4583},
  pages     = {255--271},
  publisher = {Springer},
  year      = {2007},
  url       = {https://doi.org/10.1007/978-3-540-73228-0_19},
  doi       = {10.1007/978-3-540-73228-0_19},
  timestamp = {Tue, 14 May 2019 10:00:41 +0200},
  biburl    = {https://dblp.org/rec/conf/tlca/Lindley07.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{expressive,
  author    = {Yannick Forster and
               Ohad Kammar and
               Sam Lindley and
               Matija Pretnar},
  title     = {On the expressive power of user-defined effects: Effect handlers,
               monadic reflection, delimited control},
  journal   = {J. Funct. Program.},
  volume    = {29},
  pages     = {e15},
  year      = {2019},
  url       = {https://doi.org/10.1017/S0956796819000121},
  doi       = {10.1017/S0956796819000121},
  timestamp = {Sat, 09 Apr 2022 12:29:43 +0200},
  biburl    = {https://dblp.org/rec/journals/jfp/0002KLP19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{sol,
  author    = {Makoto Hamana},
  title     = {Modular Termination Checking Theorems for Second-Order Computation},
  journal   = {CoRR},
  volume    = {abs/1912.03434},
  year      = {2019},
  url       = {http://arxiv.org/abs/1912.03434},
  eprinttype = {arXiv},
  eprint    = {1912.03434},
  timestamp = {Thu, 02 Jan 2020 18:08:18 +0100},
  biburl    = {https://dblp.org/rec/journals/corr/abs-1912-03434.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InCollection{operfl,
  author =       {Andrew Pitts and Ian Stark},
  title =        {Operational Reasoning for Functions with Local
                  State}, 
  booktitle =    {Higher Order Operational Techniques in Semantics},
  editor =       {Andrew Gordon and Andrew Pitts},
  year =         {1998},
  pages =        {227--273},
  publisher =    {Publications of the Newton Institute, Cambridge
                  University Press}, 
  url =          {http://www.inf.ed.ac.uk/~stark/operfl.html},
}

@inproceedings{altenkirch,
  author    = {Thorsten Altenkirch},
  editor    = {Georg Gottlob and
               Etienne Grandjean and
               Katrin Seyr},
  title     = {Logical Relations and Inductive/Coinductive Types},
  booktitle = {Computer Science Logic, 12th International Workshop, {CSL} '98, Annual
               Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998,
               Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1584},
  pages     = {343--354},
  publisher = {Springer},
  year      = {1998},
  url       = {https://doi.org/10.1007/10703163_23},
  doi       = {10.1007/10703163_23},
  timestamp = {Tue, 14 May 2019 10:00:42 +0200},
  biburl    = {https://dblp.org/rec/conf/csl/Altenkirch98.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{oleg,
  author    = {Oleg Kiselyov and
               Chung{-}chieh Shan},
  editor    = {Simona Ronchi Della Rocca},
  title     = {A Substructural Type System for Delimited Continuations},
  booktitle = {Typed Lambda Calculi and Applications, 8th International Conference,
               {TLCA} 2007, Paris, France, June 26-28, 2007, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4583},
  pages     = {223--239},
  publisher = {Springer},
  year      = {2007},
  url       = {https://doi.org/10.1007/978-3-540-73228-0_17},
  doi       = {10.1007/978-3-540-73228-0_17},
  timestamp = {Tue, 14 May 2019 10:00:41 +0200},
  biburl    = {https://dblp.org/rec/conf/tlca/KiselyovS07.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{Plotkin_2013,
	doi = {10.2168/lmcs-9(4:23)2013},
	url = {https://doi.org/10.2168%2Flmcs-9%284%3A23%292013},
	year = 2013,
	month = {dec},
	publisher = {Centre pour la Communication Scientifique Directe ({CCSD})},
	volume = {9},
	number = {4},
	author = {Gordon Plotkin and Matija Pretnar},
	editor = {Andrzej Tarlecki},
	title = {Handling Algebraic Effects},
	journal = {Logical Methods in Computer Science}
}

@inproceedings{monads,
  author    = {Philip Wadler},
  editor    = {Gilles Kahn},
  title     = {Comprehending Monads},
  booktitle = {Proceedings of the 1990 {ACM} Conference on {LISP} and Functional
               Programming, {LFP} 1990, Nice, France, 27-29 June 1990},
  pages     = {61--78},
  publisher = {{ACM}},
  year      = {1990},
  url       = {https://doi.org/10.1145/91556.91592},
  doi       = {10.1145/91556.91592},
  timestamp = {Fri, 06 Aug 2021 15:08:55 +0200},
  biburl    = {https://dblp.org/rec/conf/lfp/Wadler90.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{koka,
	doi = {10.4204/eptcs.153.8},
	url = {https://doi.org/10.4204%2Feptcs.153.8},
	year = 2014,
	month = {jun},
	publisher = {Open Publishing Association},
	volume = {153},
	pages = {100--126},
	author = {Daan Leijen},
	title = {Koka: Programming with Row Polymorphic Effect Types},
	journal = {Electronic Proceedings in Theoretical Computer Science}
}

@techreport{xie2020effect,
author = {Xie, Ningning and Brachthauser, Jonathan and Hillerstrom, Daniel and Schuster, Philipp and Leijen, Daan},
title = {Effect Handlers, Evidently  (Extended Version)},
institution = {Microsoft},
year = {2020},
month = {July},
abstract = {Algebraic effect handlers are a powerful way to incorporate effects in a
programming language. Sometimes perhaps even _too_ powerful. In this
article we define a restriction of general effect handlers with _scoped
resumptions_. We argue one can still express all important effects, while
improving reasoning about effect handlers. Using the newly gained
guarantees, we define a sound and coherent evidence translation for effect handlers,
which directly passes the handlers as evidence to each operation. We
prove full soundness and coherence of the translation into plain lambda calculus. The
evidence in turn enables efficient implementations of effect operations;
in particular, we show we can execute tail-resumptive operations _in
place_ (without needing to capture the evaluation context), and how we
can replace the runtime search for a handler by indexing with a constant
offset.},
url = {https://www.microsoft.com/en-us/research/publication/effect-handlers-evidently-extended-version/},
number = {MSR-TR-2020-23},
note = {Extended version of the ICFP'20 article.},
}
@book{ch,
author = {S\o{}rensen, Morten Heine and Urzyczyn, Pawel},
title = {Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics)},
year = {2006},
isbn = {0444520775},
publisher = {Elsevier Science Inc.},
address = {USA}
}
@article{lr,
  author    = {Lau Skorstengaard},
  title     = {An Introduction to Logical Relations},
  journal   = {CoRR},
  volume    = {abs/1907.11133},
  year      = {2019},
  url       = {http://arxiv.org/abs/1907.11133},
  eprinttype = {arXiv},
  eprint    = {1907.11133},
  timestamp = {Thu, 01 Aug 2019 08:59:33 +0200},
  biburl    = {https://dblp.org/rec/journals/corr/abs-1907-11133.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}