Introduction to the Course    (Preface)

Basic Proofs in Separation Logic    (Basic)

Representation Predicates    (Repr)

Heap Predicates    (Hprop)

Heap Entailment    (Himpl)

Structural Reasoning Rules    (Triples)

Reasoning Rules for Term Constructs    (Rules)

Semantics of Weakest Preconditions    (WPsem)

Weakest Precondition Generator    (WPgen)

Soundness of the Weakest Precondition Generator    (WPsound)

The Magic Wand and Other Operators    (Wand)

Affine Separation Logic    (Affine)

Reasoning about Arrays    (Arrays)

Reasoning about Records    (Records)

Conclusion and Perspectives    (Postscript)

Bibliography    (Bib)

Appendix - The Full Construction    (LibSepReference)

Appendix - Finite Maps    (LibSepFmap)

Appendix - Program Variables    (LibSepVar)

Appendix - Simplification Tactic for Entailments    (LibSepSimpl)

Appendix - Minimalistic Soundness Proof    (LibSepMinimal)