Lectures

Week	Day	Topic	Resources
1	Monday	Welcome + Judgements	Slides, Notes, Proofs Note, Lecture1
	Tuesday	Induction	Notes, Lecture2, Week1BP, Takeaways
2	Monday	Statics	Notes, Lecture3
	Tuesday	Inversion & Structural Rules	Notes, Lecture4, Week2BP, Takeaways
3	Monday	Dynamics	Notes
	Tuesday	Type safety	Notes, Takeaways
4	Monday	Functions, Effects and Calling Mechanisms	Notes, Takeaways
	Tuesday	Hoare Logic I: Triples and rules
5	Monday	Hoare Logic II: Soundness, invariants and weakest preconditions	Takeaways
	Tuesday	Separation Logic I: The heap, the separating conjunction, and the frame rule
6	Consolidation Week
7	Monday	Separation Logic II: Inductive predicates, and a proof that pays for itself	Takeaways
	Tuesday	Symbolic Execution: Under-approximation, and the logic of bugs	Takeaways
8	Monday	From Separation Logic to Rust: Ownership as a type system — and what it costs	Takeaways
	Tuesday	Ownership in Context*

*This end of the course will allow you to consolidate what you have learnt during the course in the exciting setting of a real research paper! This will be presented by Tom Divers, PhD student of the Bristol Programming Languages Research Group