Fall 2023

General Information

Lectures: 627 Seeley W. Mudd Building, Thu, 14:10-16:00

Instructor: Ronghui Gu (rg3123@columbia.edu)

Office: 515 CSB

Office hours: Thu 16:30-17:30

TA: Xupeng Li (xl2864@columbia.edu)

Location: Open Space 501

Office hours: Wed 15:00-16:00

Coq Tutorial Lectures

The materials are borrowed from the Software Foundations textbook. If you are not familiar with Coq already, you should start by working on the following chapters ASAP. Make sure you actually do all of the exercises!

Coq Tutorial

TENTATIVE Syllabus (Subject to change!)


Lecture Notes

Lecture Note 1: Introduction

Lecture Note 2: Propositional Logic