# Bibliography of Guarded Domain Theory

### Table of contents

This page collects papers and dissertations about **Guarded Domain Theory**;
if you have written a paper or dissertation on this topic, please write to me to have it added to this list.

The following authors are represented in this bibliography: Pierre America, Robert Atkey, Lars Birkedal, Aleš Bizjak, Franck Breugel, Liang-Ting Chen, Ranald Clouston, Martín Hötzel Escardó, Hans Bugge Grathwohl, Daniel Gratzer, Adrien Guatto, Robert Harper, Hsiang-Shang Ko, Magnus Baunsgaard Kristensen, Tadeusz Litak, Conor McBride, Marino Miculan, Stefan Milius, Rasmus Ejlers Møgelberg, Hiroshi Nakano, Daniele Palombi, Marco Paviotti, Jan Rutten, Jan Schwinghammer, Bas Spitters, Jonathan Sterling, Kristian Støvring, Jacob Junker Thamsborg, Daniele Turi, Niccolò Veltri, Andrea Vezzosi, and Jeroen Warmerdam.

## Refereed Publications

FSCD'22 | International Conference on Formal Structures for Computation and Deduction (FSCD) April 2022 @inproceedings{gratzer-birkedal:2022, author = {Gratzer, Daniel and Birkedal, Lars}, editor = {Felty, Amy}, address = {Dagstuhl, Germany}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, url = {https://jozefg.github.io/papers/a-stratified-approach-to-lob-induction.pdf}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, year = {2022}, month = aug, doi = {10.4230/LIPIcs.FSCD.2022.3}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {A Stratified Approach to {L\"{o}b} Induction}, volume = {228}, } |

CSL'22 | 30th EACSL Annual Conference on Computer Science Logic (CSL 2022) @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}, } |

LICS'22 | Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science @inproceedings{kristensen-mogelberg-vezzosi:2022, author = {Kristensen, Magnus Baunsgaard and M\o{}gelberg, Rasmus Ejlers and Vezzosi, Andrea}, address = {New York, NY, USA}, publisher = {Association for Computing Machinery}, booktitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science}, year = {2022}, doi = {10.48550/ARXIV.2102.01969}, title = {Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks}, } |

MFPS'21 | Proceedings 37th Conference on Mathematical Foundations of Programming Semantics @inproceedings{mogelberg-vezzosi:2021, author = {M{\o{}}gelberg, {Rasmus Ejlers} and Vezzosi, Andrea}, publisher = {Electronic Proceedings in Theoretical Computer Science}, booktitle = {Proceedings 37th Conference on Mathematical Foundations of Programming Semantics}, date = {2021-12}, doi = {10.4204/EPTCS.351.13}, pages = {200--217}, title = {Two Guarded Recursive Powerdomains for Applicative Simulation}, volume = {351}, } |

CPP'20 | Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs @inproceedings{veltri-vezzosi:2020, author = {Veltri, Niccol\`{o} and Vezzosi, Andrea}, address = {New Orleans, LA, USA}, publisher = {Association for Computing Machinery}, booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs}, year = {2020}, doi = {10.1145/3372885.3373814}, isbn = {978-1-4503-7097-4}, keywords = {ticked cubical type theory,denotational semantics,guarded recursion,pi-calculus}, pages = {270--283}, title = {Formalizing $\pi$-Calculus in {Guarded Cubical Agda}}, } |

JAR | Journal of Automated Reasoning @article{bbcgsv:2019, author = {Birkedal, Lars and Bizjak, Ale\v{s} and Clouston, Ranald and Grathwohl, Hans Bugge and Spitters, Bas and Vezzosi, Andrea}, year = {2019}, doi = {10.1007/s10817-018-9471-7}, journal = {Journal of Automated Reasoning}, number = {2}, pages = {211--253}, title = {Guarded Cubical Type Theory}, volume = {63}, } |

POPL'19 | Proceedings of the ACM on Programming Languages (POPL) January 2019 @article{mogelberg-veltri:2019, author = {M\o{}gelberg, Rasmus Ejlers and Veltri, Niccol\`{o}}, address = {New York, NY, USA}, publisher = acm, year = {2019}, month = jan, doi = {10.1145/3290317}, journal = {Proceedings of the ACM on Programming Languages}, number = {POPL}, title = {Bisimulation as Path Type for Guarded Recursive Types}, volume = {3}, } |

LICS '18 | Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18) @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}, } |

TCS | Theoretical Computer Science @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}, } |

LICS'18 | Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science @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}, } |

FICS'13 | Fundamenta Informaticae @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}, } |

FoSSaCS'16 | Foundations of Software Science and Computation Structures: 19th International Conference @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}, } |

LICS'16 | Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science @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}, } |

MFPS'15 | The 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI) @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}, } |

RTLC'14 | Rewriting and Typed Lambda Calculi -- Joint International Conference, RTA-TLCA 2014 @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}, } |

LICS'13 | Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science @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}, } |

ICFP'13 | Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming @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}, } |

LICS'11 | Proceedings of the 2011 IEEE 26th Annual Symposium on Logic in Computer Science @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}, } |

TCS | Theoretical Computer Science @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}, } |

LICS'00 | Proceedings of the Fifteenth Annual IEEE Symposium on Logic in Computer Science @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}, } |

## Unpublished Manuscripts

## Workshop Presentations

FICS'10 | Fixed Points in Computer Science 2010 @inproceedings{birkedal-schwinghammer-stovring:2010, author = {Birkedal, Lars and Scwinghammer, Jan and St{\o{}}vring, Kristian}, editor = {{ Santocanale}, {Luigi }}, booktitle = {Fixed Points in Computer Science 2010}, year = {2010}, note = {FICS 2010, the 7th Workshop on Fixed Points in Computer Science, was held in Brno, Czech Republic, on August 21-22 2010, as a satellite workshop to the conferences Mathematical Foundations of Computer Science and Computer Science Logic, 2010}, title = {A Metric Model of Lambda Calculus with Guarded Recursion}, } |

RSA'99 | Workshop on Realizability Semantics and Applications @inproceedings{escardo:1999, author = {Escard\'{o}, Mart\'{i}n}, booktitle = {Workshop on Realizability Semantics and Applications}, year = {1999}, title = {A metric model of {PCF}}, } |

REXWS'92 | Proceedings of the REX Workshop on Semantics: Foundations and Applications @inproceedings{rutten-turi:1992, author = {Rutten, Jan J. M. M. and Turi, Daniele}, address = {Berlin, Heidelberg}, publisher = {Springer-Verlag}, booktitle = {Proceedings of the REX Workshop on Semantics: Foundations and Applications}, year = {1992}, isbn = {3-540-56596-5}, pages = {477--530}, title = {On the Foundation of Final Semantics: Non-Standard Sets, Metric Spaces, Partial Orders}, } |

MFPLS'87 | Proceedings of the 3rd Workshop on Mathematical Foundations of Programming Language Semantics @inproceedings{america-rutten:1987, author = {America, Pierre and Rutten, Jan J. M. M.}, address = {Berlin, Heidelberg}, publisher = {Springer-Verlag}, booktitle = {Proceedings of the 3rd Workshop on Mathematical Foundations of Programming Language Semantics}, year = {1987}, isbn = {3-540-19020-1}, pages = {254--288}, title = {Solving Reflexive Domain Equations in a Category of Complete Metric Spaces}, } |

## Dissertations

2016 | IT-Universitetet i København @phdthesis{paviotti:2016, author = {Paviotti, Marco}, language = {English}, address = {Denmark}, school = {IT-Universitetet i K{\o{}}benhavn}, year = {2016}, isbn = {978-87-7949-345-2}, series = {ITU-DS}, title = {Denotational semantics in Synthetic Guarded Domain Theory}, } |

2016 | Aarhus University @phdthesis{bizjak:2016, author = {Bizjak, Ale\v{s}}, school = {Aarhus University}, date = {2016}, title = {On semantics and applications of guarded recursion}, } |

2015 | Institutionen för data- och informationsteknik, Datavetenskap (Chalmers), Chalmers tekniska högskola @phdthesis{vezzosi:2015, author = {Vezzosi, Andrea}, school = {Institutionen f\"{o}r data- och informationsteknik, Datavetenskap (Chalmers), Chalmers tekniska h\"{o}gskola}, year = {2015}, keywords = {induction,coinduction,totality,type theory,guarded types,sized types,Agda}, note = {63}, title = {Guarded Recursive Types in Type Theory}, } |

May 2010 | IT-Universitetet i København May 9, 2010 @phdthesis{thamsborg:2010, author = {Thamsborg, {Jacob Junker}}, address = {Denmark}, school = {IT-Universitetet i K{\o{}}benhavn}, year = {2010}, title = {Denotational World-indexed Logical Relations and Friends}, } |

## Technical Reports

1994 | CWI (Centre for Mathematics and Computer Science) @techreport{bruegel-warmerdam:1994, author = {Breugel, Franck and Warmerdam, Jeroen}, address = {NLD}, publisher = {CWI (Centre for Mathematics and Computer Science)}, year = {1994}, title = {Solving Domain Equations in a Category of Compact Metric Spaces}, } |