@article(AAG:concsp,
 author       = {Michael Gordon Abbott and Thorsten Altenkirch and Neil Ghani},
 year         = {2005},
 title        = {Containers: Constructing strictly positive types},
 journal      = {Theoretical Computer Science},
 volume       = {342},
 number       = {1},
 pages        = {3--27},
 doi          = {10.1016/j.tcs.2005.06.002},
)
@inproceedings(APTS:coppis,
 author       = {Andreas Abel and Brigitte Pientka and David Thibodeau and Anton Setzer},
 year         = {2013},
 title        = {Copatterns: programming infinite structures by observations},
 editor       = {Roberto Giacobazzi and Radhia Cousot},
 booktitle    = {Proc. of 40th Ann. {ACM} {SIGPLAN-SIGACT} Symp. on Principles of Programming Languages, {POPL}'13},
 publisher    = {{ACM}},
 pages        = {27--38},
 doi          = {10.1145/2429069.2429075},
)
@incollection(Abramsky90,
 author       = {Samson Abramsky},
 year         = {1990},
 title        = {The lazy lambda calculus},
 booktitle    = {Research topics in functional programming},
 publisher    = {Addison-Wesley Longman Publishing Co., Inc.},
 pages        = {65--116},
)
@inproceedings(ADK:parrpm,
 author       = {Thorsten Altenkirch and Nils Anders Danielsson and Nicolai Kraus},
 year         = {2017},
 title        = {Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type},
 editor       = {Javier Esparza and Andrzej S. Murawski},
 booktitle    = {Proc. of 20th Int. Conf. on Foundations of Software Science and Computation Structures, {FoSSaCS}'17},
 series       = {Lecture Notes in Computer Science},
 volume       = {10203},
 pages        = {534--549},
 doi          = {10.1007/978-3-662-54458-7\_31},
)
@inproceedings(BentonKV09,
 author       = {Nick Benton and Andrew Kennedy and Carsten Varming},
 year         = {2009},
 title        = {Some Domain Theory and Denotational Semantics in Coq},
 editor       = {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
 booktitle    = {Proc. of 22nd Int. Conf. on Theorem Proving in Higher Order Logics, TPHOLs'09},
 series       = {Lecture Notes in Computer Science},
 volume       = {5674},
 publisher    = {Springer},
 pages        = {115--130},
 doi          = {10.1007/978-3-642-03359-9\_10},
)
@article(Capretta05,
 author       = {Venanzio Capretta},
 year         = {2005},
 title        = {General recursion via coinductive types},
 journal      = {Logical Methods in Computer Science},
 volume       = {1},
 number       = {2},
 doi          = {10.2168/LMCS-1(2:1)2005},
)
@article(CUV:quodmw,
 author       = {James Chapman and Tarmo Uustalu and Niccol{\`{o}} Veltri},
 year         = {2019},
 title        = {Quotienting the delay monad by weak bisimilarity},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {29},
 number       = {1},
 pages        = {67--92},
 doi          = {10.1017/S0960129517000184},
)
@article(Dan:upttus,
 author       = {Nils Anders Danielsson},
 year         = {2018},
 title        = {Up-to techniques using sized types},
 journal      = {Proc. of {ACM} on Programming Languages},
 volume       = {2},
 number       = {{POPL}},
 pages        = {43:1--43:28},
 doi          = {10.1145/3158131},
)
@article(HasuoGeneric,
 author       = {Ichiro Hasuo},
 year         = {2015},
 title        = {Generic Weakest Precondition Semantics from Monads Enriched with Order},
 journal      = {Theoretical Computer Science},
 volume       = {604},
 number       = {C},
 pages        = {2--29},
 doi          = {10.1016/j.tcs.2015.03.047},
)
@article(Howe96,
 author       = {Douglas J. Howe},
 year         = {1996},
 title        = {Proving Congruence of Bisimulation in Functional Programming Languages},
 journal      = {Information and Computation},
 volume       = {124},
 number       = {2},
 pages        = {103\IeC{\textendash}112},
 doi          = {10.1006/inco.1996.0008},
)
@inproceedings(observation,
 author       = {P. {Johann} and A. {Simpson} and {Voigtl\IeC{\"a}nder}, J.},
 year         = {2010},
 title        = {A Generic Operational Metatheory for Algebraic Effects},
 booktitle    = {Proc. of 25th Annual IEEE Symp. on Logic in Computer Science, {LICS}'10},
 publisher    = {{IEEE} Computer Society},
 pages        = {209--218},
 doi          = {10.1109/LICS.2010.29},
)
@inproceedings(Relational,
 author       = {Ugo Dal Lago and Francesco Gavazzo and Paul Blain Levy},
 year         = {2017},
 title        = {Effectful applicative bisimilarity: Monads, relators, and Howe's method},
 booktitle    = {Proc. of 32nd Ann. {ACM/IEEE} Symp. on Logic in Computer Science, {LICS}'17},
 publisher    = {{IEEE} Computer Society},
 pages        = {1--12},
 doi          = {10.1109/LICS.2017.8005117},
)
@phdthesis(Lassen,
 author       = {S\o{}ren B. Lassen},
 year         = {1998},
 title        = {Relational Reasoning about Functions and Nondeterminism},
 school       = {University of Aarhus},
)
@article(LeroyG09,
 author       = {Xavier Leroy and Herv{\'{e}} Grall},
 year         = {2009},
 title        = {Coinductive big-step operational semantics},
 journal      = {Inf. Comput.},
 volume       = {207},
 number       = {2},
 pages        = {284--304},
 doi          = {10.1016/j.ic.2007.12.004},
)
@inproceedings(Levy11,
 author       = {Paul Blain Levy},
 year         = {2011},
 title        = {Similarity Quotients as Final Coalgebras},
 editor       = {Martin Hofmann},
 booktitle    = {Proc. of 14th Int. Conf. on Foundations of Software Science and Computational Structures, {FoSSaCS}'11},
 series       = {Lecture Notes in Computer Science},
 volume       = {6604},
 publisher    = {Springer},
 pages        = {27--41},
 doi          = {10.1007/978-3-642-19805-2\_3},
)
@article(fine-grained,
 author       = {{Paul Blain} Levy and John Power and Hayo Thielecke},
 year         = {2003},
 title        = {Modelling environments in call-by-value programming languages},
 journal      = {Information and Computation},
 volume       = {185},
 number       = {2},
 pages        = {182--210},
 doi          = {10.1016/S0890-5401(03)00088-9},
)
@mastersthesis(Matache19,
 author       = {Cristina Matache},
 year         = {2019},
 title        = {Program Equivalence for Algebraic Effects via Modalities},
 school       = {University of Oxford},
 eprint       = {1902.04645},
)
@inproceedings(MatacheS19,
 author       = {Cristina Matache and Sam Staton},
 year         = {2019},
 title        = {A Sound and Complete Logic for Algebraic Effects},
 editor       = {Mikolaj Bojanczyk and Alex Simpson},
 booktitle    = {Proc. of 22nd Int. Conf. on Foundations of Software Science and Computation Structures, {FoSSsCS}'19},
 series       = {Lecture Notes in Computer Science},
 volume       = {11425},
 publisher    = {Springer},
 pages        = {382--399},
 doi          = {10.1007/978-3-030-17127-8\_22},
)
@article(monad,
 author       = {Eugenio Moggi},
 year         = {1991},
 title        = {Notions of Computation and Monads},
 journal      = {Information and Computation},
 volume       = {93},
 number       = {1},
 pages        = {55--92},
 doi          = {10.1016/0890-5401(91)90052-4},
)
@inproceedings(Ong,
 author       = {C.{-}H. Luke Ong},
 year         = {1993},
 title        = {Non-Determinism in a Functional Setting},
 booktitle    = {Proc. of 8th Ann. Symp. on Logic in Computer Science, {LICS}'93},
 publisher    = {{IEEE} Computer Society},
 pages        = {275--286},
 doi          = {10.1109/LICS.1993.287580},
)
@inproceedings(PaviottiMB15,
 author       = {Marco Paviotti and M{\o}gelberg, Rasmus Ejlers and Lars Birkedal},
 year         = {2015},
 title        = {A Model of {PCF} in Guarded Type Theory},
 editor       = {Dan R. Ghica},
 booktitle    = {Proc. of 31st Conf. on Mathematical Foundations of Programming Semantics, {MFPS}'15},
 series       = {Electronic Notes in Theoretical Computer Science},
 volume       = {319},
 publisher    = {Elsevier},
 pages        = {333--349},
 doi          = {10.1016/j.entcs.2015.12.020},
)
@inproceedings(opsem,
 author       = {Andrew M. Pitts},
 year         = {2000},
 title        = {Operational Semantics and Program Equivalence},
 editor       = {Gilles Barthe and Peter Dybjer and Lu{\'{\i}}s Pinto and Jo{\~{a}}o Saraiva},
 booktitle    = {Adv. Lect. from Int. Summer School on Applied Semantics, {APPSEM}'00},
 series       = {Lecture Notes in Computer Science},
 volume       = {2395},
 publisher    = {Springer},
 pages        = {378--412},
 doi          = {10.1007/3-540-45699-6\_8},
)
@article(PCF,
 author       = {Gordon D. Plotkin},
 year         = {1977},
 title        = {{LCF} considered as a programming language},
 journal      = {Theoretical Computer Science},
 volume       = {5},
 number       = {3},
 pages        = {223--255},
 doi          = {10.1016/0304-3975(77)90044-5},
)
@inproceedings(effect,
 author       = {Gordon D. Plotkin and John Power},
 year         = {2001},
 title        = {Adequacy for Algebraic Effects},
 editor       = {Furio Honsell and Marino Miculan},
 booktitle    = {Proc. of 4th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS'01},
 series       = {Lecture Notes in Computer Science},
 volume       = {2030},
 pages        = {1--24},
 doi          = {10.1007/3-540-45315-6\_1},
)
@article(Handlers,
 author       = {Gordon D. Plotkin and Matija Pretnar},
 year         = {2013},
 title        = {Handling Algebraic Effects},
 journal      = {Log.\ Methods Comput.\ Sci.},
 volume       = {9},
 number       = {4, article 23},
 pages        = {1--36},
 doi          = {10.2168/lmcs-9(4:23)2013},
)
@inproceedings(Pnueli77,
 author       = {Amir Pnueli},
 year         = {1977},
 title        = {The Temporal Logic of Programs},
 booktitle    = {Proc. of 18th Ann. Symp. on Foundations of Computer Science, {FOCS}'77},
 publisher    = {{IEEE} Computer Society},
 pages        = {46--57},
 doi          = {10.1109/SFCS.1977.32},
)
@article(modal-journal,
 author       = {Alex Simpson and Niels Voorneveld},
 year         = {2020},
 title        = {Behavioural Equivalence via Modalities for Algebraic Effects},
 journal      = {ACM Transactions on Programming Languages and Systems},
 volume       = {42},
 number       = {1},
 pages        = {4:1--4:45},
 doi          = {10.1145/3363518},
)
@article(VMA:cubadt,
 author       = {Andrea Vezzosi and Anders M{\"{o}}rtberg and Andreas Abel},
 year         = {2019},
 title        = {Cubical {A}gda: a dependently typed programming language with univalence and higher inductive types},
 journal      = {Proc. of {ACM} on Programming Languages},
 volume       = {3},
 number       = {{ICFP}},
 pages        = {87:1--87:29},
 doi          = {10.1145/3341691},
)
@phdthesis(VoorneveldThesis,
 author       = {Niels Voorneveld},
 year         = {2020},
 title        = {Equality between programs with effects},
 school       = {University of Ljubljana},
)
@article(XiaZHHMPZ20,
 author       = {Li{-}yao Xia and Yannick Zakowski and Paul He and Chung{-}Kil Hur and Gregory Malecha and Benjamin C. Pierce and Steve Zdancewic},
 year         = {2020},
 title        = {Interaction trees: representing recursive and impure programs in Coq},
 journal      = {Proc. {ACM} Program. Lang.},
 volume       = {4},
 number       = {{POPL}},
 pages        = {51:1--51:32},
 doi          = {10.1145/3371119},
)