Program Logics for Certified Compilers

1. Introduction; Part I. Generic Separation Logic: 2. Hoare logic; 3. Separation logic; 4. Soundness of Hoare logic; 5. Mechanized semantic library Andrew W. Appel, Robert Dockins and Aquinas Hobor; 6. Separation algebras; 7. Operators on separation algebras; 8. First-order separation logic; 9. A little case study; 10. Covariant recursive predicates; 11. Share accounting; Part II. Higher-Order Separation Logic: 12. Separation logic as a logic; 13. From separation algebras to separation logic; 14. Simplification by rewriting; 15. Introduction to step-indexing; 16. Predicate implication and subtyping; 17. General recursive predicates; 18. Case study: separation logic with first-class functions; 19. Data structures in indirection theory; 20. Applying higher-order separation logic; 21. Lifted separation logics; Part III. Separation Logic for CompCert: 22. Verifiable C; 23. Expressions, values, and assertions; 24. The VST separation logic for C light; 25. Typechecking for Verifiable C Josiah Dodds; 26. Derived rules and proof automation for C light; 27. Proof of a program; 28. More C programs; 29. Dependently typed C programs; 30. Concurrent separation logic; Part IV. Operational Semantics of CompCert: 31. CompCert; 32. The CompCert memory model Xavier Leroy, Andrew W. Appel, Sandrine Blazy and Gordon Stewart; 33. How to specify a compiler Lennart Beringer, Robert Dockins and Gordon Stewart; 34. C light operational semantics; Part V. Higher-Order Semantic Models: 35. Indirection theory Aquinas Hobor, Andrew Appel and Robert Dockins; 36. Case study: lambda-calculus with references; 37. Higher-order Hoare logic; 38. Higher-order separation logic; 39. Semantic models of predicates-in-the-heap; Part VI. Semantic Model and Soundness of Verifiable C: 40. Separation algebra for CompCert; 41. Share models; 42. Juicy memories Gordon Stewart and Andrew W. Appel; 43. Modeling the Hoare judgment; 44. Semantic model of CSL; 45. Modular structure of the development; Part VII. Applications: 46. Foundational static analysis; 47. Heap theorem prover Gordon Stewart, Lennart Beringer and Andrew W. Appel.