TrainLogic: Logic and Type theory

This course of lectures is an introduction to logic and type theory as background material for formal methods.

Topics

Lambda Calculus

  1. introducing transition system rules for a while programming language
  2. expanding to procedures and recursion (eager evaluation)
  3. syntax of LC, bound and free variables, currying, substitution
  4. beta reduction, lambda calculus rules
  5. church numerals, pairs, fixed points, while
  6. equivalence, eta reduction, normal forms
  7. Church-Rosser property

Logic

  1. introduction to propositional natural deduction
  2. truth tables, normal forms, satisfiability
  3. functions, relations, terms, satisfaction
  4. quantifiers and natural deduction inference
  5. states, assertions, invariants
  6. theories
  7. predicate transformers
  8. Hoare logic

Set theory

  1. Zermelo-Fraenkel: ideas and axioms
  2. specification and first-order logic
  3. unions, products, equinumerousness
  4. function space, powerset, diagonal argument
  5. relations, reflexive transitive closure
  6. equivalences, partitions
  7. the axiom of choice and transfinite induction

Type theory

  1. typed languages
  2. function types: simply typed lambda calculus
  3. product types and Currying
  4. natural numbers, recursive definitions including function valued (e.g. Ackermann functions)
  5. parametric types (poymorphism)
  6. inductive types
  7. dependent types
  8. propositions as types; integrated

References

  1. Ian chiswell and Wilfrid Hodges, Mathematical Logic
  2. Ebbinghaus, Flum and Thomas, Mathematical Logic, Springer-Verlag.
  3. David Gries, The science of programming
  4. Martin-Lof, Intutionist Type Theory.
  5. Hindley and Seldin Lambda-Calculus and Combinators: An Introduction, Cambridge.
  6. John Reynolds, Theories of programming languages.
  7. Halmos, Naive set theory.
  8. Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Studies, Princeton 2013; available at http://homotopytypetheory.org/book/.

Software installation (Idris)

For the Type Theory segment, I recommend installing Idris. Using Idris is pleasant, but installation can be painful. On Windows, I suggest using the binary on that page. If you are using linux, you may find this answer helpful (i.e., use stack).

Course Details

Lecture Slides

Exercises