References

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