4. Week 04: Logics for Functional Programs¶

The lecture will be given by Kiran Gopinathan.

4.1. Mandatory Reading¶

Logics for Funcitonal, Higher-Order Languages (by Xavier Leroy)

4.2. Accompanying Code¶

CFML and F* Verification Examples

4.3. Recommended Reading¶

Arthur Charguéraud: Characteristic Formulae for the Verification of Imperative Programs, 2011
Nikhil Swamy et al.: Verifying Higher-order Programs with the Dijkstra Monad, 2013