Logique de séparation en Coq : théorie et pratique