Bibliography of Guarded Domain Theory

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
To appear A stratified approach to Löb induction
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
Realising Intensional S4 and GL Modalities
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
Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks
M. B. Kristensen, R. E. Møgelberg, and A. Vezzosi
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
Two Guarded Recursive Powerdomains for Applicative Simulation
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
Formalizing π-Calculus in Guarded Cubical Agda
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
Guarded Cubical Type Theory
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
Bisimulation as Path Type for Guarded Recursive Types
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
Guarded Computational Type Theory
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
A model of guarded recursion via generalised equilogical spaces
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
A Generalized Modality for Recursion
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
Guard Your Daggers and Traces: On The Equational Properties of Guarded (Co-)recursion
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
Guarded Dependent Type Theory with Coinductive Types
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
Denotational Semantics of Recursive Types in Synthetic Guarded Domain Theory
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
A Model of PCF in Guarded Type Theory
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
A Model of Countable Nondeterminism in Guarded Type Theory
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
Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes
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
Productive Coprogramming with Guarded Recursion
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
First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees
L. Birkedal, R. E. Møgelberg, J. Schwinghammer, and K. Støvring
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
The Category-Theoretic Solution of Recursive Metric-Space Equations
L. Birkedal, K. Støvring, and J. J. Thamsborg
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
A modality for recursion
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

Apr. 2022
Preprint Classifying topoi in synthetic guarded domain theory: the universal property of multi-clock guarded recursion
April 19, 2022
@unpublished{palombi-sterling:2022,
  author = {Palombi, Daniele and Sterling, Jonathan},
  url = {https://www.jonmsterling.com/papers/palombi-sterling:2022.pdf},
  year = {2022},
  month = mar,
  note = {Unpublished manuscript},
  title = {Classifying topoi in synthetic guarded domain theory},
}

Workshop Presentations

FICS'10
A Metric Model of Lambda Calculus with Guarded Recursion
L. Birkedal, J. Schwinghammer, and K. Støvring
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
A metric model of PCF
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
On the Foundation of Final Semantics: Non-Standard Sets, Metric Spaces, Partial Orders
J. Rutten and D. Turi
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
Solving Reflexive Domain Equations in a Category of Complete Metric Spaces
P. America and J. Rutten
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
Denotational semantics in Synthetic Guarded Domain Theory
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
On semantics and applications of guarded recursion
Aarhus University
@phdthesis{bizjak:2016,
  author = {Bizjak, Ale\v{s}},
  school = {Aarhus University},
  date = {2016},
  title = {On semantics and applications of guarded recursion},
}
2015
Guarded Recursive Types in Type Theory
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
Denotational World-indexed Logical Relations and Friends
J. J. Thamsborg
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
Solving Domain Equations in a Category of Compact Metric Spaces
F. Breugel and J. Warmerdam
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},
}