MoSeL: a general, extensible modal framework for interactive proofs in separation logic

Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung 0002, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer. MoSeL: a general, extensible modal framework for interactive proofs in separation logic. Proceedings of the ACM on Programming Languages, 2(ICFP), 2018. [doi]

@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},
}