@article(abramsky1990lazy,
 author       = {Samson Abramsky},
 year         = {1990},
 title        = {The lazy lambda calculus, Research topics in functional programming},
)
@book(domain:handbook,
 author       = {Samson Abramsky and Achim Jung},
 year         = {1994},
 title        = {Domain theory},
 publisher    = {Oxford University Press},
)
@inproceedings(ahman2020runners,
 author       = {Danel Ahman and Andrej Bauer},
 year         = {2020},
 title        = {Runners in action},
 booktitle    = {European Symposium on Programming},
 organization = {Springer, Cham},
 pages        = {29--55},
 doi          = {10.1007/978-3-030-44914-8_2},
)
@article(Appel:M01,
 author       = {Andrew W. Appel and David McAllester},
 year         = {2001},
 title        = {An indexed model of recursive types for foundational proof-carrying code},
 journal      = {ACM Trans. Program. Lang. Syst},
 volume       = {23},
 number       = {5},
 pages        = {657--683},
 doi          = {10.1145/504709.504712},
)
@article(apt1986countable,
 author       = {Krzysztof R Apt and Gordon D Plotkin},
 year         = {1986},
 title        = {Countable nondeterminism and random assignment},
 journal      = {Journal of the ACM (JACM)},
 volume       = {33},
 number       = {4},
 pages        = {724--767},
 doi          = {10.1145/6490.6494},
)
@article(atkey13icfp,
 author       = {Robert Atkey and Conor McBride},
 year         = {2013},
 title        = {Productive coprogramming with guarded recursion},
 journal      = {ACM SIGPLAN Notices},
 volume       = {48},
 number       = {9},
 pages        = {197--208},
 doi          = {10.1145/2544174.2500597},
)
@inproceedings(bahr2017clocks,
 author       = {Patrick Bahr. and Hans Bugge Grathwohl and M{\o}gelberg, Rasmus Ejlers},
 year         = {2017},
 title        = {The clocks are ticking: No more delays!},
 booktitle    = {2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
 organization = {IEEE},
 pages        = {1--12},
 doi          = {10.1109/LICS.2017.8005097},
)
@article(BasoldGW17,
 author       = {Henning Basold and Herman Geuvers and Niels van der Weide},
 year         = {2017},
 title        = {Higher Inductive Types in Programming},
 journal      = {J. Univers. Comput. Sci.},
 volume       = {23},
 number       = {1},
 pages        = {63--88},
 url          = {http://www.jucs.org/jucs\_23\_1/higher\_inductive\_types\_in},
)
@inproceedings(benton2009some,
 author       = {Nick Benton and Andrew Kennedy and Carsten Varming},
 year         = {2009},
 title        = {Some domain theory and denotational semantics in Coq},
 booktitle    = {International Conference on Theorem Proving in Higher Order Logics},
 organization = {Springer},
 pages        = {115--130},
 doi          = {10.1007/978-3-642-03359-9_10},
)
@article(ToT,
 author       = {Lars Birkedal and M{\o}gelberg, Rasmus Ejlers and Jan Schwinghammer and St{\o}vring, Kristian},
 year         = {2012},
 title        = {First steps in synthetic guarded domain theory: step-indexing in the topos of trees},
 journal      = {Logical Methods in Computer Science},
 volume       = {8},
 number       = {4},
 doi          = {10.2168/LMCS-8(4:1)2012},
)
@incollection(Bizjak:TLCA:2014,
 author       = {Ale\v{s} Bizjak and Lars Birkedal and Marino Miculan},
 year         = {2014},
 title        = {A Model of Countable Nondeterminism in Guarded Type Theory},
 booktitle    = {Rewriting and Typed Lambda Calculi},
 publisher    = {Springer},
 pages        = {108--123},
 doi          = {10.1007/978-3-319-08918-8_8},
)
@article(capretta:lifting,
 author       = {Venanzio Capretta},
 year         = {2005},
 title        = {{General Recursion via Coinductive Types}},
 journal      = {{Logical Methods in Computer Science}},
 volume       = {{Volume 1, Issue 2}},
 doi          = {10.2168/LMCS-1(2:1)2005},
)
@article(quotientingDelay,
 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},
)
@inproceedings(CTT,
 author       = {Cyril Cohen and Thierry Coquand and Simon Huber and Anders M{\"o}rtberg},
 year         = {2018},
 title        = {Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom},
 booktitle    = {21st International Conference on Types for Proofs and Programs (TYPES 2015)},
 organization = {Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik},
 doi          = {10.4230/LIPIcs.TYPES.2015.5},
)
@inproceedings(dal2017effectful,
 author       = {Dal Lago, Ugo and Francesco Gavazzo and Paul Blain Levy},
 year         = {2017},
 title        = {Effectful applicative bisimilarity: Monads, relators, and Howe's method},
 booktitle    = {2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
 organization = {IEEE},
 pages        = {1--12},
 doi          = {10.1109/LICS.2017.8005117},
)
@inproceedings(danielsson2012operational,
 author       = {Nils Anders Danielsson},
 year         = {2012},
 title        = {Operational semantics using the partiality monad},
 booktitle    = {Proceedings of the 17th ACM SIGPLAN international conference on Functional programming},
 pages        = {127--138},
 doi          = {10.1145/2364527.2364546},
)
@article(di1995uncountable,
 author       = {Di Gianantonio, Pietro and Furio Honsell and Gordon Plotkin},
 year         = {1995},
 title        = {Uncountable limits and the lambda calculus},
)
@inproceedings(dockins2014formalized,
 author       = {Robert Dockins},
 year         = {2014},
 title        = {Formalized, effective domain theory in coq},
 booktitle    = {International Conference on Interactive Theorem Proving},
 organization = {Springer},
 pages        = {209--225},
 doi          = {10.1007/978-3-319-08970-6_14},
)
@inproceedings(FGGW18,
 author       = {Dan Frumin and Herman Geuvers and L{\'{e}}on Gondelman and Niels van der Weide},
 year         = {2018},
 title        = {Finite sets in homotopy type theory},
 editor       = {June Andronick and Amy P. Felty},
 booktitle    = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January 8-9, 2018},
 publisher    = {{ACM}},
 pages        = {201--214},
 doi          = {10.1145/3167085},
)
@inproceedings(howe1989equality,
 author       = {Douglas J Howe},
 year         = {1989},
 title        = {Equality in lazy computation systems},
 booktitle    = {LICS},
 volume       = {89},
 pages        = {198--203},
 doi          = {10.1109/LICS.1989.39174},
)
@article(hyland2006discrete,
 author       = {Martin Hyland and John Power},
 year         = {2006},
 title        = {Discrete Lawvere theories and computational effects},
 journal      = {Theoretical Computer Science},
 volume       = {366},
 number       = {1-2},
 pages        = {144--162},
 doi          = {10.1016/j.tcs.2006.07.007},
)
@inproceedings(dejong:CSL:2021,
 author       = {Tom de Jong and Mart{\'\iota}n H{\"o}tzel Escard{\'o}},
 year         = {2021},
 title        = {{Domain Theory in Constructive and Predicative Univalent Foundations}},
 editor       = {Christel Baier and Goubault-Larrecq, Jean},
 booktitle    = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
 series       = {Leibniz International Proceedings in Informatics (LIPIcs)},
 volume       = {183},
 publisher    = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
 address      = {Dagstuhl, Germany},
 pages        = {28:1--28:18},
 doi          = {10.4230/LIPIcs.CSL.2021.28},
)
@inproceedings(kraus14,
 author       = {Nicolai Kraus},
 year         = {2014},
 title        = {The General Universal Property of the Propositional Truncation},
 editor       = {Hugo Herbelin and Pierre Letouzey and Matthieu Sozeau},
 booktitle    = {20th International Conference on Types for Proofs and Programs, {TYPES} 2014, May 12-15, 2014, Paris, France},
 series       = {LIPIcs},
 volume       = {39},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 pages        = {111--145},
 doi          = {10.4230/LIPIcs.TYPES.2014.111},
)
@misc(kristensen2021model,
 author       = {Magnus Baunsgaard Kristensen and M\IeC{\o}gelberg, Rasmus Ejlers and Andrea Vezzosi},
 year         = {2021},
 title        = {Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks},
 eprint       = {2102.01969},
)
@article(lassen1998similarity,
 author       = {S{\o}ren B Lassen and Corin S Pitcher},
 year         = {1998},
 title        = {Similarity and bisimilarity for countable non-determinism and higher-order functions},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {10},
 pages        = {246--266},
 doi          = {10.1016/S1571-0661(05)80704-2},
)
@phdthesis(lassen1998relational,
 author       = {S{\o}ren B{\o}gh Lassen},
 year         = {1998},
 title        = {Relational reasoning about functions and nondeterminism},
 school       = {University of Aarhus},
)
@article(clottmodel,
 author       = {Bassel Mannaa and M{\o}gelberg, Rasmus Ejlers and Niccol{\`o} Veltri},
 year         = {2020},
 title        = {{Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory}},
 journal      = {Logical Methods in Computer Science},
 volume       = {16},
 doi          = {10.23638/LMCS-16(4:17)2020},
)
@inproceedings(GDTT:FPC,
 author       = {M{\o}gelberg, Rasmus Ejlers and Marco Paviotti},
 year         = {2016},
 title        = {Denotational semantics of recursive types in synthetic guarded domain theory},
 booktitle    = {LICS},
 doi          = {10.1145/2933575.2934516},
)
@article(mogelbergPOPL2019,
 author       = {M{\o}gelberg, Rasmus Ejlers and Niccol{\`o} Veltri},
 year         = {2019},
 title        = {Bisimulation as path type for guarded recursive types},
 journal      = {Proceedings of the ACM on Programming Languages},
 volume       = {3},
 number       = {POPL},
 pages        = {1--29},
 doi          = {10.1145/3290317},
)
@article(moggi1991notions,
 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(ong1993non,
 author       = {C-HL Ong},
 year         = {1993},
 title        = {Non-determinism in a functional setting},
 booktitle    = {[1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science},
 organization = {IEEE},
 pages        = {275--286},
 doi          = {10.1109/LICS.1993.287580},
)
@article(paviottiPCF,
 author       = {Marco Paviotti and M{\o}gelberg, Rasmus Ejlers and Lars Birkedal},
 year         = {2015},
 title        = {A model of PCF in guarded type theory},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {319},
 pages        = {333--349},
 doi          = {10.1016/j.entcs.2015.12.020},
)
@article(pitts1996relational,
 author       = {Andrew M Pitts},
 year         = {1996},
 title        = {Relational properties of domains},
 journal      = {Information and computation},
 volume       = {127},
 number       = {2},
 pages        = {66--90},
 doi          = {10.1006/inco.1996.0052},
)
@article(pitts1997note,
 author       = {Andrew M Pitts},
 year         = {1997},
 title        = {A note on logical relations between semantics and syntax},
 journal      = {Logic Journal of the IGPL},
 volume       = {5},
 number       = {4},
 pages        = {589--601},
 doi          = {10.1093/jigpal/5.4.589},
)
@article(schwinghammer2013step,
 author       = {Jan Schwinghammer and Ale{\v{s}} Bizjak and Lars Birkedal},
 year         = {2013},
 title        = {Step-indexed relational reasoning for countable nondeterminism},
 journal      = {Logical Methods in Computer Science},
 volume       = {9},
 doi          = {10.2168/LMCS-9(4:4)2013},
)
@book(hottbook,
 author       = {{Univalent Foundations Program}, The},
 year         = {2013},
 title        = {Homotopy Type Theory: Univalent Foundations of Mathematics},
 publisher    = {\url{https://homotopytypetheory.org/book}},
 address      = {Institute for Advanced Study},
)
@article(uustalu2015stateful,
 author       = {Tarmo Uustalu},
 year         = {2015},
 title        = {Stateful runners of effectful computations},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {319},
 pages        = {403--421},
 doi          = {10.1016/j.entcs.2015.12.024},
)
@article(CubicalAgda,
 author       = {Andrea Vezzosi and Anders M{\"o}rtberg and Andreas Abel},
 year         = {2019},
 title        = {Cubical Agda: a dependently typed programming language with univalence and higher inductive types},
 journal      = {Proceedings of the ACM on Programming Languages},
 volume       = {3},
 number       = {ICFP},
 pages        = {1--29},
 doi          = {10.1145/3341691},
)
@article(xia2019interaction,
 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         = {2019},
 title        = {Interaction trees: representing recursive and impure programs in Coq},
 journal      = {Proceedings of the ACM on Programming Languages},
 volume       = {4},
 number       = {POPL},
 pages        = {1--32},
 doi          = {10.1145/3371119},
)