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]