Interactive proofs in higher-order concurrent separation logic
Robbert Krebbers, Amin Timany, Lars Birkedal · 2016
When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they are cluttered with bookkeeping code related to manipulating the object logic.