Paviotti, Marco; Bengtson, Jesper Formally verifying exceptions for low-level code with separation logic. (English) Zbl 1382.68053 J. Log. Algebr. Methods Program. 94, 1-14 (2018). MSC: 68N30 03B70 68Q60 68T15 × Cite Format Result Cite Review PDF Full Text: DOI Link
Naumann, David A. Towards patterns for heaps and imperative lambdas. (English) Zbl 1355.68040 J. Log. Algebr. Methods Program. 85, No. 5, Part 2, 1038-1056 (2016). MSC: 68N18 × Cite Format Result Cite Review PDF Full Text: DOI arXiv