CSC 579 Spring 2023
(R 9:40am to 10:55 Lechase 103)

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.