CSC535: Overview: Syllabus [5/21]

1. Foundations 
   1.1 Functional programming 
   1.2 Inductive definitions and proof techniques 
   1.3 Constructive logic 
   1.4 The Coq proof assistant 

2. Reasoning about programs
   2.1 Specifying a simple imperative language
   2.2 Operational semantics
   2.3 Hoare Logic
   2.4 Information-flow security (*)

3. Type systems
   3.1 Simply typed lambda-calculus
   3.2 Type safety
   3.3 Subtyping (*)

(*) If time permits