InstructorProf. Suresh Jagannathan Room 3154J Lawson Computer Science Building Ph: x4-0971 suresh@cs.purdue.edu Office Hours: Tu, Th. 4 - 5PM |

A detailed syllabus can be found here.

- Course Overview
- Download Software Foundations
- Download Coq 8.5
- Download Proof General or CoqIde
- Fill in "Admits" in Basics.v from Software Foundations.

- Finish exercises in Basics. A particularly interesting exercise you should be comfortable solving is starsM (alternative number representation).

- Induction
- Lists
- Problem Set 1. Due Sept. 7th.

- No class.

- Polymorphism (cont)
- Tactics
- Homework 1. Due Sept. 19th.

- Logic (cont.)
- Problem Set 2. Due Sept. 28th.

- Inductively Defined Propositions (cont)
- Maps
- Homework 2. Due Oct. 5.

- The Imp Language (cont.)
- Problem Set 3. Due Oct. 26.

- Hoare Logic (cont.)
- Homework 3. Due Nov. 2.

- Smallstep Semantics
- Problem Set 4. Due Nov. 28.