Bibliography of Guarded Domain Theory

@inproceedings{chen-ko:2022,
  author = {Chen, Liang-Ting and Ko, Hsiang-Shang},
  editor = {Manea, Florin and Simpson, Alex},
  address = {Dagstuhl, Germany},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f\"{u}r Informatik},
  booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  year = {2022},
  doi = {10.4230/LIPIcs.CSL.2022.14},
  isbn = {978-3-95977-218-1},
  issn = {1868-8969},
  pages = {14:1--14:17},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {{Realising Intensional S4 and GL Modalities}},
  volume = {216},
}

@article{bizjak-mogelberg:2020,
  author = {Bizjak, Ale\v{s} and M\o{}gelberg, Rasmus Ejlers},
  publisher = {Cambridge University Press,
  year = {2020},
  doi = {10.1017/S0960129520000080},
  journal = {Mathematical Structures in Computer Science},
  number = {4},
  pages = {342--378},
  title = {Denotational semantics for guarded dependent type theory},
  volume = {30},
}

@article{bizjak-birkedal:2018,
  author = {Bizjak, Ale\v{s} and Birkedal, Lars},
  year = {2018},
  doi = {10.1016/j.entcs.2018.03.016},
  journal = {Electronic Notes in Theoretical Computer Science},
  pages = {57--78},
  title = {On Models of Higher-Order Separation Logic},
  volume = {336},
}

@inproceedings{sterling-harper:2018,
 author = {Sterling, Jonathan and Harper, Robert},
 title = {Guarded Computational Type Theory},
 booktitle = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
 series = {LICS '18},
 year = {2018},
 isbn = {978-1-4503-5583-4},
 location = {Oxford, United Kingdom},
 pages = {879--888},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/3209108.3209153},
 doi = {10.1145/3209108.3209153},
 acmid = {3209153},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {clocks, dependent types, guarded recursion, operational semantics, type theory},
}

@article{bizjak-birkedal:2018:tcs,
  author = {Bizjak, Ale\v{s} and Birkedal, Lars},
  date = {2018},
  doi = {10.1016/j.tcs.2018.02.012},
  issn = {0304-3975},
  journaltitle = {Theoretical Computer Science},
  keywords = {Semantics,Dependent type theory,Guarded recursion,Equilogical spaces},
  pages = {1--18},
  title = {A model of guarded recursion via generalised equilogical spaces},
  volume = {722},
}

@inproceedings{guatto:2018,
  author = {Guatto, Adrien},
  booktitle = {Proceedings of the 33rd Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS} 2018, Oxford, UK, July 09-12, 2018},
  year = {2018},
  doi = {10.1145/3209108.3209148},
  pages = {482--491},
  title = {A Generalized Modality for Recursion},
}

@article{milius-litak:2017,
  author = {Milius, Stefan and Litak, Tadeusz},
  publisher = {IOS Press},
  year = {2017},
  doi = {10.3233/FI-2017-1475},
  journal = {Fundamenta Informaticae},
  number = {3-4},
  pages = {407--449},
  title = {Guard Your Daggers and Traces: Properties of Guarded (Co-)recursion},
  volume = {150},
}

@inproceedings{bgcmb:2016,
  author = {Bizjak, Ale\v{s} and Grathwohl, Hans Bugge and Clouston, Ranald and M{\o{}}gelberg, Rasmus E. and Birkedal, Lars},
  editor = {Jacobs, Bart and L\"{o}ding, Christof},
  address = {Berlin, Heidelberg},
  publisher = {Springer Berlin Heidelberg},
  booktitle = {Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2--8, 2016, Proceedings},
  year = {2016},
  doi = {10.1007/978-3-662-49630-5_2},
  eprint = {1601.01586},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
  isbn = {978-3-662-49630-5},
  pages = {20--35},
  title = {Guarded Dependent Type Theory with Coinductive Types},
}

@inproceedings{mogelberg-paviotti:2016,
  author = {M\o{}gelberg, Rasmus Ejlers and Paviotti, Marco},
  address = {New York, NY, USA},
  publisher = {Association for Computing Machinery},
  booktitle = {Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science},
  year = {2016},
  doi = {10.1145/2933575.2934516},
  isbn = {978-1-4503-4391-6},
  pages = {317--326},
  title = {Denotational Semantics of Recursive Types in Synthetic Guarded Domain Theory},
}

@article{paviotti-mogelberg-birkedal:2015,
  author = {Paviotti, Marco and M\o{}gelberg, Rasmus Ejlers and Birkedal, Lars},
  year = {2015},
  doi = {10.1016/j.entcs.2015.12.020},
  issn = {1571-0661},
  journal = {Electronic Notes in Theoretical Computer Science},
  keywords = {Denotational semantics,guarded recursion,type theory,PCF,synthetic domain theory},
  note = {The 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI)},
  number = {Supplement C},
  pages = {333--349},
  title = {A Model of {PCF} in {Guarded Type Theory}},
  volume = {319},
}

@inproceedings{bizjak-birkedal-miculan:2014,
  author = {Bizjak, Ales and Birkedal, Lars and Miculan, Marino},
  editor = {Dowek, Gilles},
  publisher = {Springer},
  booktitle = {Rewriting and Typed Lambda Calculi -- Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings},
  year = {2014},
  doi = {10.1007/978-3-319-08918-8_8},
  isbn = {978-3-319-08917-1},
  pages = {108--123},
  series = {Lecture Notes in Computer Science},
  title = {A Model of Countable Nondeterminism in Guarded Type Theory},
  volume = {8560},
}

@inproceedings{birkedal-mogelberg:2013,
  author = {Birkedal, L. and M{\o{}}gelberg, R. E.},
  address = {Washington, DC, USA},
  publisher = {IEEE Computer Society},
  booktitle = {Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science},
  year = {2013},
  doi = {10.1109/LICS.2013.27},
  isbn = {978-0-7695-5020-6},
  issn = {1043-6871},
  pages = {213--222},
  title = {Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes},
}

@inproceedings{atkey-mcbride:2013,
  author = {Atkey, Robert and McBride, Conor},
  address = {Boston, Massachusetts, USA},
  publisher = acm,
  booktitle = {Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming},
  year = {2013},
  doi = {10.1145/2500365.2500597},
  isbn = {978-1-4503-2326-0},
  keywords = {coalgebras,corecursion,guarded recursion,total functional programming},
  pages = {197--208},
  title = {Productive Coprogramming with Guarded Recursion},
}

@inproceedings{bmss:2011,
  author = {Birkedal, Lars and M{\o{}}gelberg, Rasmus Ejlers and Schwinghammer, Jan and St\o{}vring, Kristian},
  address = {Washington, DC, USA},
  publisher = {IEEE Computer Society},
  booktitle = {Proceedings of the 2011 IEEE 26th Annual Symposium on Logic in Computer Science},
  year = {2011},
  doi = {10.1109/LICS.2011.16},
  eprint = {1208.3596},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
  isbn = {978-0-7695-4412-0},
  pages = {55--64},
  title = {First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees},
}

@article{birkedal-stovring-thamsborg:2010,
  author = {Birkedal, Lars and St\o{}vring, Kristian and Thamsborg, Jacob},
  address = {GBR},
  publisher = {Elsevier Science Publishers Ltd.},
  year = {2010},
  month = oct,
  doi = {10.1016/j.tcs.2010.07.010},
  issn = {0304-3975},
  journal = {Theoretical Computer Science},
  number = {47},
  pages = {4102--4122},
  title = {The Category-Theoretic Solution of Recursive Metric-Space Equations},
  volume = {411},
}

@inproceedings{nakano:2000,
  author = {Nakano, Hiroshi},
  address = {New York},
  publisher = {IEEE Computer Society},
  booktitle = {Proceedings of the Fifteenth Annual IEEE Symposium on Logic in Computer Science},
  year = {2000},
  doi = {10.1109/LICS.2000.855774},
  issn = {1043-6871},
  pages = {255--266},
  title = {A modality for recursion},
}

@article{arnold-nivat:1980,
  author = {Arnold, A. and Nivat, M.},
  year = {1980},
  doi = {10.1016/0304-3975(80)90045-6},
  issn = {0304-3975},
  journal = {Theoretical Computer Science},
  number = {2},
  pages = {181--205},
  title = {Metric interpretations of infinite trees and semantics of non deterministic recursive programs},
  volume = {11},
}