Abstract
The fourth seminar delved into the mechanization of a separation logic, a subject that the fourth lecture had only just touched upon. The speaker showed how to build such a logic in Coq from a natural semantics for a small language of the " mini-ML " type, i.e. an extended functional language with mutable references. He then described several tools, still integrated into Coq, that facilitate program verification : a weaker precondition calculus, data structure encoding predicates, and Coq tactics. All these elements can be found in his CFML tool for imperative program verification.
