Logic, Programs & Verification

COMP 4600/5300 - 201

At a glance...

Progress Report Due Date
Midterm Check-in March, 17
Final Check-in April, 30

Week 1: Preliminaries

Reading

  • Preface: Preface.v

Exercises

  • Get Coq up and running on your system
  • Download Software Foundations source files
  • Create your git repository for solutions and proofs

Week 2: Functional Programming

Reading

  • Functional Programming in Coq: Basics.v

Topics

  • Basic types, enumerations, numbers, booleans
  • Functions and recursion
  • Unit tests

Exercises

  • Standard: All 1 and 2 star

Week 3: Induction

Reading

  • Proof by Induction: Induction.v

Topics

  • Inductive proof tactics, structured proofs
  • Local assertions
  • Formal vs informal proofs

Exercises

  • Standard: All 2 star
  • Advanced: All 3 star
  • Challenge: bin_nat_bin