Interactive proofs in higher-order concurrent separation logic.

Robbert Krebbers, Amin Timany, Lars Birkedal

Browse the full POPL paper archive.