Logic for Proofs and Programs (CS3234)

• Prelude
• Updates
• Lecture Notes, Week 01
  • The events leading to the term project and the oral exams
  • Introduction and motivation
  • Soundness and completeness
  • Functional programming in Gallina
  • Polymorphism in Gallina
  • Exercises for Week 01
  • Index of concepts for Week 01
• Lecture Notes, Week 02
  • Formalizing a proof with the Coq Proof Assistant
  • The intro tactic
  • The revert tactic
  • Proving logical properties with the Coq Proof Assistant
  • Exercises for Week 02
  • Index of concepts for Week 02
• Lecture Notes, Week 03
  • Warmup
  • The rewrite tactic
  • Structural induction over Peano numbers
  • The exists tactic
  • Specifications
  • Structural induction over binary trees
  • Exercises for Week 03
  • Index of concepts for Week 03
• Lecture Notes, Week 04
  • Specifications that depend on other specifications
  • More about soundness and completeness
  • Proving the soundness of unit tests
  • Backward and forward proofs
  • Reasoning equationally about recursive functions using fold-unfold lemmas
  • Reasoning about arithmetical functions
  • Exercises for Week 04
  • Index of concepts for Week 04
• Lecture Notes, Week 05
  • Lambda-lifting and lambda-dropping
  • Structuring programs, structuring proofs
  • Two more goodies to go
  • Induction and induction proofs: a recapitulation
  • Mystery functions
  • Tidbits, and some advice to boot
  • Exercises for Week 05
  • Index of concepts for Week 05
• Lecture Notes, Week 06
  • About unfolding calls
  • The exists tactic, revisited
  • Ex falso quodlibet
  • Soundness and completeness of equality predicates
  • A simple problem
  • The situation so far
  • Exercises for Week 06
  • Index of concepts for Week 06
• Midterm project
  • Expectations about the midterm project
  • A study of polymorphic lists and primitive iteration
  • Index of concepts for the midterm project
• Lecture Notes, Week 07
  • Life after the midterm project
  • Functional equality
  • A study of isometries in the equilateral triangle
  • Soundness and completeness of equality predicates, revisited
  • The case of proofs by cases
  • Exercises for Week 07
  • Index of concepts for Week 07
• Lecture Notes, Week 08
  • More tactics
  • The Euclidean division
  • Exercises for Week 08
  • Index of concepts for Week 08
• Lecture Notes, Week 09
  • Formalizing informal proofs
  • Exercises for Week 09
• Lecture Notes, Week 10
  • A Fibonacci structure
  • The abstraction and instantiation of Eureka lemmas about resetting the accumulator
  • Exercises for Week 10
  • Index of concepts for Week 10
• Lecture Notes, Week 11
  • The functional abstraction and instantiation of recursive functions
  • The functional abstraction and instantiation of tail-recursive functions that use an accumulator
  • Tail-recursive functions are recursive
  • Primitive recursion
  • Exercises for Week 11
  • Index of concepts for Week 11
• Lecture Notes, Week 12
  • Curry and uncurry
  • Induction principles
  • Induction principles, continued
  • Mutual induction and recursion
  • Exercises for Week 12
  • Index of concepts for Week 12
• Lecture Notes, Week 13
  • A continuation-based interpreter
  • Exercises for Week 13
• Term project
  • Expectations about the term project
  • Three language processors for arithmetic expressions
• Tools
  • GNU Emacs
  • Coq
  • Proof General
• Dramatis Personæ
  • In real life (Computer Science)
  • In real life (before Computer Science)
  • In real life (outside Computer Science)
  • Fictional (main characters)
  • Fictional (recurring)
  • Fictional (others)
  • Version
• Songbook
  • Hacking the Coq SSR
  • My, my (hey hey)
  • Hey hey (my, my)
  • Funky tree
• Postlude