@inproceedings{KrebbersPS16,
  title = {Moessner's Theorem: An Exercise in Coinductive Reasoning in Coq},
  author = {Robbert Krebbers and Louis Parlant and Alexandra Silva},
  year = {2016},
  doi = {10.1007/978-3-319-30734-3_21},
  url = {http://dx.doi.org/10.1007/978-3-319-30734-3_21},
  researchr = {https://researchr.org/publication/KrebbersPS16},
  cites = {0},
  citedby = {0},
  pages = {309-324},
  booktitle = {Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday},
  editor = {Erika Ábrahám and Marcello M. Bonsangue and Einar Broch Johnsen},
  volume = {9660},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-30733-6},
}

@inproceedings{0002KBD16,
  title = {Higher-order ghost state},
  author = {Ralf Jung 0002 and Robbert Krebbers and Lars Birkedal and Derek Dreyer},
  year = {2016},
  doi = {10.1145/2951913.2951943},
  url = {http://doi.acm.org/10.1145/2951913.2951943},
  researchr = {https://researchr.org/publication/0002KBD16},
  cites = {0},
  citedby = {0},
  pages = {256-269},
  booktitle = {Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016},
  editor = {Jacques Garrigue and Gabriele Keller and Eijiro Sumii},
  publisher = {ACM},
  isbn = {978-1-4503-4219-3},
}

@inproceedings{Krebbers14-0,
  title = {Separation Algebras for C Verification in Coq},
  author = {Robbert Krebbers},
  year = {2014},
  doi = {10.1007/978-3-319-12154-3_10},
  url = {http://dx.doi.org/10.1007/978-3-319-12154-3_10},
  researchr = {https://researchr.org/publication/Krebbers14-0},
  cites = {0},
  citedby = {0},
  pages = {150-166},
  booktitle = {Verified Software: Theories, Tools and Experiments - 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers},
  editor = {Dimitra Giannakopoulou and Daniel Kroening},
  volume = {8471},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-12153-6},
}

@article{GeuversKM13,
  title = {T-calculus},
  author = {Herman Geuvers and Robbert Krebbers and James McKinna},
  year = {2013},
  doi = {10.1016/j.apal.2012.05.005},
  url = {http://dx.doi.org/10.1016/j.apal.2012.05.005},
  researchr = {https://researchr.org/publication/GeuversKM13},
  cites = {0},
  citedby = {0},
  journal = {Annals of Pure and Applied Logic},
  volume = {164},
  number = {6},
  pages = {676-701},
}

@article{GeuversK11,
  title = {The correctness of Newman s typability algorithm and some of its extensions},
  author = {Herman Geuvers and Robbert Krebbers},
  year = {2011},
  doi = {10.1016/j.tcs.2011.03.016},
  url = {http://dx.doi.org/10.1016/j.tcs.2011.03.016},
  researchr = {https://researchr.org/publication/GeuversK11},
  cites = {0},
  citedby = {0},
  journal = {Theoretical Computer Science},
  volume = {412},
  number = {28},
  pages = {3242-3261},
}

@article{BizjakGKB19,
  title = {Iron: managing obligations in higher-order concurrent separation logic},
  author = {Ales Bizjak and Daniel Gratzer and Robbert Krebbers and Lars Birkedal},
  year = {2019},
  url = {https://dl.acm.org/citation.cfm?id=3290378},
  researchr = {https://researchr.org/publication/BizjakGKB19},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
}

@article{JungJKD18,
  title = {RustBelt: securing the foundations of the rust programming language},
  author = {Ralf Jung and Jacques-Henri Jourdan and Robbert Krebbers and Derek Dreyer},
  year = {2018},
  doi = {10.1145/3158154},
  url = {http://doi.acm.org/10.1145/3158154},
  researchr = {https://researchr.org/publication/JungJKD18},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {2},
  number = {POPL},
}

@inproceedings{KrebbersTB17,
  title = {Interactive proofs in higher-order concurrent separation logic},
  author = {Robbert Krebbers and Amin Timany and Lars Birkedal},
  year = {2017},
  url = {http://dl.acm.org/citation.cfm?id=3009855},
  researchr = {https://researchr.org/publication/KrebbersTB17},
  cites = {0},
  citedby = {0},
  pages = {205-217},
  booktitle = {Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017},
  editor = {Giuseppe Castagna and Andrew D. Gordon},
  publisher = {ACM},
  isbn = {978-1-4503-4660-3},
}

@article{KrebbersJ0TKTCD18,
  title = {MoSeL: a general, extensible modal framework for interactive proofs in separation logic},
  author = {Robbert Krebbers and Jacques-Henri Jourdan and Ralf Jung 0002 and Joseph Tassarotti and Jan-Oliver Kaiser and Amin Timany and Arthur Charguéraud and Derek Dreyer},
  year = {2018},
  doi = {10.1145/3236772},
  url = {https://doi.org/10.1145/3236772},
  researchr = {https://researchr.org/publication/KrebbersJ0TKTCD18},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {2},
  number = {ICFP},
}

@inproceedings{Krebbers14,
  title = {An operational and axiomatic semantics for non-determinism and sequence points in C},
  author = {Robbert Krebbers},
  year = {2014},
  doi = {10.1145/2535838.2535878},
  url = {http://doi.acm.org/10.1145/2535838.2535878},
  researchr = {https://researchr.org/publication/Krebbers14},
  cites = {0},
  citedby = {0},
  pages = {101-112},
  booktitle = {The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014},
  editor = {Suresh Jagannathan and Peter Sewell},
  publisher = {ACM},
  isbn = {978-1-4503-2544-8},
}

@inproceedings{Krebbers0BJDB17,
  title = {The Essence of Higher-Order Concurrent Separation Logic},
  author = {Robbert Krebbers and Ralf Jung 0002 and Ales Bizjak and Jacques-Henri Jourdan and Derek Dreyer and Lars Birkedal},
  year = {2017},
  doi = {10.1007/978-3-662-54434-1_26},
  url = {http://dx.doi.org/10.1007/978-3-662-54434-1_26},
  researchr = {https://researchr.org/publication/Krebbers0BJDB17},
  cites = {0},
  citedby = {0},
  pages = {696-723},
  booktitle = {Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings},
  editor = {Hongseok Yang},
  volume = {10201},
  series = {Lecture Notes in Computer Science},
  isbn = {978-3-662-54434-1},
}

@inproceedings{RouvoetPKV20,
  title = {Intrinsically-typed definitional interpreters for linear, session-typed languages},
  author = {Arjen Rouvoet and Casper Bach Poulsen and Robbert Krebbers and Eelco Visser},
  year = {2020},
  doi = {10.1145/3372885.3373818},
  url = {https://doi.org/10.1145/3372885.3373818},
  researchr = {https://researchr.org/publication/RouvoetPKV20},
  cites = {0},
  citedby = {0},
  pages = {284-298},
  booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020},
  editor = {Jasmin Blanchette and Catalin Hritcu},
  publisher = {ACM},
  isbn = {978-1-4503-7097-4},
}

@article{Krebbers16,
  title = {A Formal C Memory Model for Separation Logic},
  author = {Robbert Krebbers},
  year = {2016},
  doi = {10.1007/s10817-016-9369-1},
  url = {http://dx.doi.org/10.1007/s10817-016-9369-1},
  researchr = {https://researchr.org/publication/Krebbers16},
  cites = {0},
  citedby = {0},
  journal = {Journal of Automated Reasoning},
  volume = {57},
  number = {4},
  pages = {319-387},
}

@article{HinrichsenBK20,
  title = {Actris: session-type based reasoning in separation logic},
  author = {Jonas Kastberg Hinrichsen and Jesper Bengtson and Robbert Krebbers},
  year = {2020},
  doi = {10.1145/3371074},
  url = {https://doi.org/10.1145/3371074},
  researchr = {https://researchr.org/publication/HinrichsenBK20},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {4},
  number = {POPL},
}

@inproceedings{KrebbersW11,
  title = {A Formalization of the C99 Standard in HOL, Isabelle and Coq},
  author = {Robbert Krebbers and Freek Wiedijk},
  year = {2011},
  doi = {10.1007/978-3-642-22673-1_28},
  url = {http://dx.doi.org/10.1007/978-3-642-22673-1_28},
  researchr = {https://researchr.org/publication/KrebbersW11},
  cites = {0},
  citedby = {0},
  pages = {301-303},
  booktitle = {Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings},
  editor = {James H. Davenport and William M. Farmer and Josef Urban and Florian Rabe},
  volume = {6824},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-22672-4},
}

@article{PoulsenRTKV18,
  title = {Intrinsically-typed definitional interpreters for imperative languages},
  author = {Casper Bach Poulsen and Arjen Rouvoet and Andrew P. Tolmach and Robbert Krebbers and Eelco Visser},
  year = {2018},
  doi = {10.1145/3158104},
  url = {http://doi.acm.org/10.1145/3158104},
  tags = {Intrinsic-Verification},
  researchr = {https://researchr.org/publication/PoulsenRTKV18},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {2},
  number = {POPL},
}

@techreport{preprint-PoulsenRTKV18,
  title = {Intrinsically-typed definitional interpreters for imperative languages},
  author = {Casper Bach Poulsen and Arjen Rouvoet and Andrew P. Tolmach and Robbert Krebbers and Eelco Visser},
  year = {2018},
  researchr = {https://researchr.org/publication/preprint-PoulsenRTKV18},
  cites = {0},
  citedby = {0},
  type = {Preprint},
}

@inproceedings{KrebbersW13,
  title = {Separation Logic for Non-local Control Flow and Block Scope Variables},
  author = {Robbert Krebbers and Freek Wiedijk},
  year = {2013},
  doi = {10.1007/978-3-642-37075-5_17},
  url = {http://dx.doi.org/10.1007/978-3-642-37075-5_17},
  researchr = {https://researchr.org/publication/KrebbersW13},
  cites = {0},
  citedby = {0},
  pages = {257-272},
  booktitle = {Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings},
  editor = {Frank Pfenning},
  volume = {7794},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-37074-8},
}

@inproceedings{KrebbersLW14,
  title = {Formal C Semantics: CompCert and the C Standard},
  author = {Robbert Krebbers and Xavier Leroy and Freek Wiedijk},
  year = {2014},
  doi = {10.1007/978-3-319-08970-6_36},
  url = {http://dx.doi.org/10.1007/978-3-319-08970-6_36},
  researchr = {https://researchr.org/publication/KrebbersLW14},
  cites = {0},
  citedby = {0},
  pages = {543-548},
  booktitle = {Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings},
  editor = {Gerwin Klein and Ruben Gamboa},
  volume = {8558},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-08969-0},
}

@inproceedings{Krebbers13,
  title = {Aliasing Restrictions of C11 Formalized in Coq},
  author = {Robbert Krebbers},
  year = {2013},
  doi = {10.1007/978-3-319-03545-1_4},
  url = {http://dx.doi.org/10.1007/978-3-319-03545-1_4},
  researchr = {https://researchr.org/publication/Krebbers13},
  cites = {0},
  citedby = {0},
  pages = {50-65},
  booktitle = {Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
  editor = {Georges Gonthier and Michael Norrish},
  volume = {8307},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-03544-4},
}

@article{KaiserZKRD18,
  title = {Mtac2: typed tactics for backward reasoning in Coq},
  author = {Jan-Oliver Kaiser and Beta Ziliani and Robbert Krebbers and Yann Régis-Gianas and Derek Dreyer},
  year = {2018},
  doi = {10.1145/3236773},
  url = {https://doi.org/10.1145/3236773},
  researchr = {https://researchr.org/publication/KaiserZKRD18},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {2},
  number = {ICFP},
}

@inproceedings{KrebbersS11,
  title = {Computer Certified Efficient Exact Reals in Coq},
  author = {Robbert Krebbers and Bas Spitters},
  year = {2011},
  doi = {10.1007/978-3-642-22673-1_7},
  url = {http://dx.doi.org/10.1007/978-3-642-22673-1_7},
  researchr = {https://researchr.org/publication/KrebbersS11},
  cites = {0},
  citedby = {0},
  pages = {90-106},
  booktitle = {Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings},
  editor = {James H. Davenport and William M. Farmer and Josef Urban and Florian Rabe},
  volume = {6824},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-22672-4},
}

@article{JungKJBBD18,
  title = {Iris from the ground up: A modular foundation for higher-order concurrent separation logic},
  author = {Ralf Jung 0002 and Robbert Krebbers and Jacques-Henri Jourdan and Ales Bizjak and Lars Birkedal and Derek Dreyer},
  year = {2018},
  doi = {10.1017/S0956796818000151},
  url = {https://doi.org/10.1017/S0956796818000151},
  researchr = {https://researchr.org/publication/JungKJBBD18},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {28},
}

@inbook{RouvoetAPKV20-ext,
  title = {Knowing When to Ask: Sound scheduling of name resolution in type checkers derived from declarative specifications (Extended Version)},
  author = {Arjen Rouvoet and Hendrik van Antwerpen and Casper Bach Poulsen and Robbert Krebbers and Eelco Visser},
  year = {2020},
  month = {Oct},
  doi = {10.5281/zenodo.4091445},
  url = {http://doi.org/10.5281/zenodo.4091445},
  researchr = {https://researchr.org/publication/RouvoetAPKV20-ext},
  cites = {0},
  citedby = {0},
  publisher = {Zenodo},
}

@inproceedings{FruminKB18,
  title = {ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency},
  author = {Dan Frumin and Robbert Krebbers and Lars Birkedal},
  year = {2018},
  doi = {10.1145/3209108.3209174},
  url = {http://doi.acm.org/10.1145/3209108.3209174},
  researchr = {https://researchr.org/publication/FruminKB18},
  cites = {0},
  citedby = {0},
  pages = {442-451},
  booktitle = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018},
  editor = {Anuj Dawar and Erich Grädel},
  publisher = {ACM},
}

@inproceedings{KrebbersW15,
  title = {A Typed C11 Semantics for Interactive Theorem Proving},
  author = {Robbert Krebbers and Freek Wiedijk},
  year = {2015},
  doi = {10.1145/2676724.2693571},
  url = {http://doi.acm.org/10.1145/2676724.2693571},
  researchr = {https://researchr.org/publication/KrebbersW15},
  cites = {0},
  citedby = {0},
  pages = {15-27},
  booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015},
  editor = {Xavier Leroy and Alwen Tiu},
  publisher = {ACM},
  isbn = {978-1-4503-3296-5},
}

@inproceedings{FruminGK19,
  title = {Semi-automated Reasoning About Non-determinism in C Expressions},
  author = {Dan Frumin and Léon Gondelman and Robbert Krebbers},
  year = {2019},
  doi = {10.1007/978-3-030-17184-1_3},
  url = {https://doi.org/10.1007/978-3-030-17184-1_3},
  researchr = {https://researchr.org/publication/FruminGK19},
  cites = {0},
  citedby = {0},
  pages = {60-87},
  booktitle = {Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings},
  editor = {Luís Caires},
  volume = {11423},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-030-17184-1},
}