MoSeL: a general, extensible modal framework for interactive proofs in separation logic.
Robbert KrebbersJacques-Henri JourdanRalf JungJoseph TassarottiJan-Oliver KaiserAmin TimanyArthur CharguéraudDerek DreyerPublished in: Proc. ACM Program. Lang. (2018)