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.