CSC 579 Spring 2026
(R 9:40am to 10:55 Douglass 307)

The language of intelligence is logic. The course teaches proof systems, with a focus on Coq. You will learn to use Coq to formalize logic, which is the fundamental language of rational thought and problem-solving, and construct sound and verifiable proofs. A similar system, Lean 4, was used by generative AI, Alpha Proof, to solve Olympiad-level math problems. By learning the fundamentals of modern proof systems, you acquire a complete foundation for logical thinking and the knowledge and skill to use or build automated reasoning systems.

Pre-requisites: Students enrolling in the course are expected to have advanced knowledge in either programming languages (CSC 253, 254 or 255), math, or logic.

Syllabus

• The Need for Training Thought: The Values of Thought. Tendencies Needing Constant Regulation.  Regulation Transforms Inference into Proof.
• Type Systems.  Operational Semantics. Progress. Type Preservation. Type Soundness.
• Functional Programming in Coq: Data and Functions.  Proof by Simplification, Rewriting and Case Analysis.
• Proof by Induction. Proofs Within Proofs.  Formal vs. Informal Proof.
• Lists, Options, Partial Maps.
• Basic Tactics: apply, apply with, injection, discriminate, unfold, destruct.
• Logic in Coq. Logical Connectives: Conjunction, Disjunction, Falsehood and Negation, Truth, Logical Equivalence, Logical Equivalence, Existential Quantification.  Programming with Propositions. Applying Theorems to Arguments. Coq vs. Set Theory: Functional Extensionality, Propositions vs. Booleans, Classical vs. Constructive Logic.
• Inductively Defined Propositions. Induction Principles for Propositions.  Induction Over an Inductively Defined Set and an Inductively Defined Proposition.
• The Curry-Howard Correspondence. Natural Deduction. Typed Lambda Calculus. Proof Scripts. Quantifiers, Implications, Functions. Logical Connectives as Inductive Types.