↢ Back to the List of Courses

COMP 4901X - Formal Reasoning about Programs

Summer Semester 2022-23

Number of Students: 44 

Average Rating by the Students: 5.0/5.0 

YouTube Playlist

https://youtube.com/playlist?list=PLzZlJT-UOiwCTvmi68ilVWNfwhl_7DphI&si=mFs_0IXe0Eav5_T8 

Course Files

https://drive.google.com/drive/folders/1XKt2jJ-MBopG6m2G8TpYYcIfHSz4nw6V

Assignments

• Homework 1

  • hw1.v

• Homework 2

  • hw2.v

• Final Exam

Course Contents

• Lectures 1 and 2: Operational Semantics (Video Recording)

  • Small-step Operational Semantics (Slides)

  • Big-step Operational Semantics (Slides)

• Lectures 3 and 4: Introduction to Coq (Video Recording)

  • scratchpad.v

  • ex1.v

  • ex2.v

  • ex3.v

  • ex4.v

  • ex5.v

  • frobenius.v

  • frobenius-dual.v

• Lectures 5 and 6: Denotational Semantics (Video Recording)

  • Denotational Semantics (Slides)

• Lecture 7: Hoare Logic (Video Recording)

  • Hoare Logic (Slides)

  • Read the Wikipedia article on Hoare Logic

• Lecture 8 - Games on Graphs (Video Recording)

  • Games on Graphs (Slides)

• Lectures 9 and 10 - Solving Büchi and Parity Games (Video Recording)

  • Classical Algorithm for Büchi Games (Slides)

  • Quadratic Algorithm for Büchi Games (Slides)

  • Inductive Algorithm for Parity Games (Slides)

• Lectures 11 and 12: Inductive Reasoning and Types in Coq (Video Recording)

  • basic-coq.v

  • induction.v

• Lectures 13 and 14 - Büchi Automata on Infinite Words (Video Recording)

  • Automata on Infinite Words (Slides)

  • Set Operations on Büchi Automata (Slides)

• Lectures 15 and 16 - Linear-time Temporal Logic (Video Recording) 

  • Linear Temporal Logic (Slides)

  • LTL to NBW Translation (Slides)

  • LTL to NBW Translation (More Examples) 

• Lectures 17 and 18: Lists, Options and Polymorphism in Coq (Video Recording)

  • lists-polymorphism.v

• Lectures 19 and 20: Higher-order Functions and Further Tactics in Coq

  • further-tactics.v

• A Useful Textbook for Coq

• Lectures 21 and 22: Further Training in Coq (Video Recording)

  • programs.v

• Lectures 23 and 24: Defining the WHILE language in Coq (Video Recording)

• Lectures 25 and 26: Small-step Semantics and Hoare Logic in Coq (Video Recording) 

  • hoare.v