Introduction

Computing Science is mathematical science. Fundamental to all problem- solving is the ability to construct solutions, and verify their correctness. Com- puter science uses formal systems to formulate problem solutions (aka programs) and to analyse and verify them. This course focuses on the mathematical tools, primarily constructive logic and category theory, used to describe the semantics of programming languages. This firm foundation for program construction and verification supports our most important class of programs: programming lan- guage implementations. Indeed, the current trend in programming languages research is toward increasingly rigorous mechanized metatheory: “Soon, papers will be rejected from POPL because they didn’t include mechanically-checked proofs of the properties claimed.”

This course introduces the students to

• proof theory: proofs as formal objects of study, including
  • natural deduction and sequent styles
  • logical connectives as proof combinators
  • rules of reasoning as proof transformations
  • automated and semi-automated proof construction
• type theory: types as specifications of programs, including
  • mapping inductive datatypes into symbolic logic formulae
  • mapping program statements into proof term transformations, leading to the Curry-Howard correspondence: programs as proofs of well- formed propositions via type analysis
• partially-ordered sets and lattices:
  • for characterizing recursion and fixed points (and hence iterative and non-terminating programs)
  • leading to static analysis and approximation, especially in the for- mulation of projection/concretization pairs as Galois connections
• and ending with the underlying category theory, yielding an insight into
  • monoids as programming constructs,
  • closed cartesian categories as models of lambda-calculus,
  • Floyd/Hoare type theory for showing formal correctness.

Textbooks

Most of the material comes from the first four chapters of the textbook. Based upon interest of the students and available time, additional material from chap- ters 5 and 6 may be presented.

Required

• Paul Taylor, Practical Foundations of Mathematics, Cambridge Studies in Advanced Mathematics, Cambridge University Press, 1999; text available online.

Supplemental

• Yves Bertot and Pierre Casteran, Interactive Theorem Proving and Program Development, Springer, 2004.
• Benjamin Pierce, Basic Category Theory for Computer Scientists, MIT Press, 1991.

Software

• Coq v. 8.3, inria, http://coq.inria.fr.
• Proof-General v. 4, Edinburgh (http://proofgeneral.inf.ed.ac.uk).

Staff

Instructor: Chris Dutchyn
email mailto:dutchyn@cs.usask.ca
web http://www.cs.usask.ca/faculty/cjd032
office Thorvaldson 178.2

Meetings

Weekly, 3 hour meetings comprising 1.5 hours of lecture/presentation and 1.5 hours of discussion and worked exercises and examples.

Grading

Regular attendance and productive classroom participation is mandatory for this reading-group-like course. There will be four assignments, drawn from questions from the four chapters of the textbook. In addition, the students will be asked to present assignment solutions, to encourage classrom participation and develop skill in communicating deep technical material to a well-prepared audience. In addition, the students will need to read, summarize, and present a recent research paper in the area.

Sitting In

Students cannot unofficially audit (sit-in on) the meetings. Because much of the course entails in-class discussion, anyone sitting-in would complete the sub- stantive work of the course, and merits credit for that effort.