A talk on soundness of concurrent separation logic by using coq is given at IPSJ PRO workshop
A talk on “Proof of Soundness of Concurrent Separation Logic for GPGPU in Coq” is given by Izumi Asakura, Hidehiko Masuhara, and Tomoyuki Aotani at the 104th IPSJ PRO workshop.
