@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},
)