@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 = {BIRTHDAY},
}

@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 = {ICFP},
}

@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 = {vstte},
}

@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 = {APAL},
  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 = {TCS},
  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 = {PACMPL},
  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 = {PACMPL},
  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 = {POPL},
}

@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 = {PACMPL},
  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 = {POPL},
}

@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 = {ESOP},
}

@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 = {CPP},
}

@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 = {JAR},
  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 = {PACMPL},
  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 = {mkm},
}

@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 = {PACMPL},
  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 = {fossacs},
}

@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 = {itp},
}

@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 = {CPP},
}

@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 = {PACMPL},
  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 = {mkm},
}

@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 = {JFP},
  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 = {lics},
}

@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 = {CPP},
}

@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 = {ESOP},
}