Separation Logic Course

This webpage provides material for the second part of Course 2-36-1 "Proof of Program", MPRI 2017-2018. (Material for the first part can be found on Fran├žois Bobot's webpage). This second part teaches fundamentals of separation logic and the corresponding proof methods.

Plan

Previous exams

You may have a look at the exam for 2016-2017. You may even look at some of the solutions, once you actually had a serious go at the exercises.

Previous exams:

Installation instructions for interactive proofs

# STEP 1 (~15 minutes)
# if you don't have it, install opam with ocaml 4.05.0

sudo apt-get install unzip m4 aspcud
wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin
eval `opam config env`
opam switch 4.05.0 # should be the default switch anyway
eval `opam config env`


# STEP 2 (~40 minutes)
# if you don't have it, install Coq 8.6.1
# (Coq 8.7.0 and Coq 8.7.1 work as well)

opam install coq.8.6.1

#if you want coqide and run into problem, try installing libgtksourceview2.0-dev and then coqide
sudo apt-get install libgtksourceview2.0-dev
opam install coqide


# STEP 3 (~1 minute)
# download and build course

mkdir mpri_sep_course
cd mpri_sep_course
wget https://madiot.fr/sepcourse.zip
unzip sepcourse.zip
make -j # this should fail for file Repr.v


# STEP 4
# play with Hprop.v and then Repr.v

coqide Hprop.v
coqide Repr.v
# you can run emacs instead of coqide if you have with proof general installed