References

  1. Samson Abramsky (1990): The lazy lambda calculus, Research topics in functional programming.
  2. Samson Abramsky & Achim Jung (1994): Domain theory. Oxford University Press.
  3. Danel Ahman & Andrej Bauer (2020): Runners in action. In: European Symposium on Programming. Springer, Cham, pp. 29–55, doi:10.1007/978-3-030-44914-8_2.
  4. Andrew W. Appel & David McAllester (2001): An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst 23(5), pp. 657–683, doi:10.1145/504709.504712.
  5. Krzysztof R Apt & Gordon D Plotkin (1986): Countable nondeterminism and random assignment. Journal of the ACM (JACM) 33(4), pp. 724–767, doi:10.1145/6490.6494.
  6. Robert Atkey & Conor McBride (2013): Productive coprogramming with guarded recursion. ACM SIGPLAN Notices 48(9), pp. 197–208, doi:10.1145/2544174.2500597.
  7. Patrick Bahr., Hans Bugge Grathwohl & Rasmus Ejlers Møgelberg (2017): The clocks are ticking: No more delays!. In: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, pp. 1–12, doi:10.1109/LICS.2017.8005097.
  8. Henning Basold, Herman Geuvers & Niels van der Weide (2017): Higher Inductive Types in Programming. J. Univers. Comput. Sci. 23(1), pp. 63–88. Available at http://www.jucs.org/jucs_23_1/higher_inductive_types_in.
  9. Nick Benton, Andrew Kennedy & Carsten Varming (2009): Some domain theory and denotational semantics in Coq. In: International Conference on Theorem Proving in Higher Order Logics. Springer, pp. 115–130, doi:10.1007/978-3-642-03359-9_10.
  10. Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer & Kristian Støvring (2012): First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science 8(4), doi:10.2168/LMCS-8(4:1)2012.
  11. Aleš Bizjak, Lars Birkedal & Marino Miculan (2014): A Model of Countable Nondeterminism in Guarded Type Theory. In: Rewriting and Typed Lambda Calculi. Springer, pp. 108–123, doi:10.1007/978-3-319-08918-8_8.
  12. Venanzio Capretta (2005): General Recursion via Coinductive Types. Logical Methods in Computer Science Volume 1, Issue 2, doi:10.2168/LMCS-1(2:1)2005.
  13. 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.
  14. Cyril Cohen, Thierry Coquand, Simon Huber & Anders Mörtberg (2018): Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In: 21st International Conference on Types for Proofs and Programs (TYPES 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, doi:10.4230/LIPIcs.TYPES.2015.5.
  15. Ugo Dal Lago, Francesco Gavazzo & Paul Blain Levy (2017): Effectful applicative bisimilarity: Monads, relators, and Howe's method. In: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, pp. 1–12, doi:10.1109/LICS.2017.8005117.
  16. Nils Anders Danielsson (2012): Operational semantics using the partiality monad. In: Proceedings of the 17th ACM SIGPLAN international conference on Functional programming, pp. 127–138, doi:10.1145/2364527.2364546.
  17. Pietro Di Gianantonio, Furio Honsell & Gordon Plotkin (1995): Uncountable limits and the lambda calculus.
  18. Robert Dockins (2014): Formalized, effective domain theory in coq. In: International Conference on Interactive Theorem Proving. Springer, pp. 209–225, doi:10.1007/978-3-319-08970-6_14.
  19. Dan Frumin, Herman Geuvers, Léon Gondelman & Niels van der Weide (2018): Finite sets in homotopy type theory. In: June Andronick & Amy P. Felty: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018. ACM, pp. 201–214, doi:10.1145/3167085.
  20. Douglas J Howe (1989): Equality in lazy computation systems. In: LICS 89, pp. 198–203, doi:10.1109/LICS.1989.39174.
  21. Martin Hyland & John Power (2006): Discrete Lawvere theories and computational effects. Theoretical Computer Science 366(1-2), pp. 144–162, doi:10.1016/j.tcs.2006.07.007.
  22. Tom de Jong & Mart\'ιn Hötzel Escardó (2021): Domain Theory in Constructive and Predicative Univalent Foundations. In: Christel Baier & Jean Goubault-Larrecq: 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), Leibniz International Proceedings in Informatics (LIPIcs) 183. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, pp. 28:1–28:18, doi:10.4230/LIPIcs.CSL.2021.28.
  23. Nicolai Kraus (2014): The General Universal Property of the Propositional Truncation. In: Hugo Herbelin, Pierre Letouzey & Matthieu Sozeau: 20th International Conference on Types for Proofs and Programs, TYPES 2014, May 12-15, 2014, Paris, France, LIPIcs 39. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 111–145, doi:10.4230/LIPIcs.TYPES.2014.111.
  24. Magnus Baunsgaard Kristensen, Rasmus Ejlers M\IeCø gelberg & Andrea Vezzosi (2021): Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks. ArXiv:2102.01969.
  25. Søren B Lassen & Corin S Pitcher (1998): Similarity and bisimilarity for countable non-determinism and higher-order functions. Electronic Notes in Theoretical Computer Science 10, pp. 246–266, doi:10.1016/S1571-0661(05)80704-2.
  26. Søren Bøgh Lassen (1998): Relational reasoning about functions and nondeterminism. University of Aarhus.
  27. Bassel Mannaa, Rasmus Ejlers Møgelberg & Niccolò Veltri (2020): Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory. Logical Methods in Computer Science 16, doi:10.23638/LMCS-16(4:17)2020.
  28. Rasmus Ejlers Møgelberg & Marco Paviotti (2016): Denotational semantics of recursive types in synthetic guarded domain theory. In: LICS, doi:10.1145/2933575.2934516.
  29. Rasmus Ejlers Møgelberg & Niccolò Veltri (2019): Bisimulation as path type for guarded recursive types. Proceedings of the ACM on Programming Languages 3(POPL), pp. 1–29, doi:10.1145/3290317.
  30. Eugenio Moggi (1991): Notions of computation and monads. Information and computation 93(1), pp. 55–92, doi:10.1016/0890-5401(91)90052-4.
  31. C-HL Ong (1993): Non-determinism in a functional setting. In: [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science. IEEE, pp. 275–286, doi:10.1109/LICS.1993.287580.
  32. Marco Paviotti, Rasmus Ejlers Møgelberg & Lars Birkedal (2015): A model of PCF in guarded type theory. Electronic Notes in Theoretical Computer Science 319, pp. 333–349, doi:10.1016/j.entcs.2015.12.020.
  33. Andrew M Pitts (1996): Relational properties of domains. Information and computation 127(2), pp. 66–90, doi:10.1006/inco.1996.0052.
  34. Andrew M Pitts (1997): A note on logical relations between semantics and syntax. Logic Journal of the IGPL 5(4), pp. 589–601, doi:10.1093/jigpal/5.4.589.
  35. Jan Schwinghammer, Aleš Bizjak & Lars Birkedal (2013): Step-indexed relational reasoning for countable nondeterminism. Logical Methods in Computer Science 9, doi:10.2168/LMCS-9(4:4)2013.
  36. The Univalent Foundations Program (2013): Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study.
  37. Tarmo Uustalu (2015): Stateful runners of effectful computations. Electronic Notes in Theoretical Computer Science 319, pp. 403–421, doi:10.1016/j.entcs.2015.12.024.
  38. Andrea Vezzosi, Anders Mörtberg & Andreas Abel (2019): Cubical Agda: a dependently typed programming language with univalence and higher inductive types. Proceedings of the ACM on Programming Languages 3(ICFP), pp. 1–29, doi:10.1145/3341691.
  39. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C Pierce & Steve Zdancewic (2019): Interaction trees: representing recursive and impure programs in Coq. Proceedings of the ACM on Programming Languages 4(POPL), pp. 1–32, doi:10.1145/3371119.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org