**McMaster University — Graduate Course CAS 763**

**Winter 2021**

**Dr. Wolfram Kahl**,
ITB-245 , ext: 27042,
`kahl``@``mcmaster.ca`.

Dependent types are everywhere in mathematics —
you probably don't even notice them.
But can you implement a matrix multiplication function
in C, C++, Java, Rust, Go, Standard ML, OCaml, or Haskell 2010
such that the *type system* will catch attempts to multiply
a 3-by-4 matrix with a 2-by-5 matrix?
Dependent types can encode such constraints, and much more:
Via the Curry-Howard correspondence, specifications expressed
as logical formulae can be turned into types, so that the type checker
can be used to guarantee data-type invariants and program correctness:
Programs that are not proven correct then won't even compile!

The course CAS 763 will help you to learn the dependently-typed programming language Agda, practice formalising the mathematics needed for expressing datatype invariants and program specifications, and also acquire knowledge and understanding of the relevant foundations.

Previous experience with Haskell wold be useful, but is not strictly necessary. Familiarity with basic propositional and predicate logic is essentially assumed.

Type systems featuring types depending on values empower not only logics that can capture common mathematical formalisations more naturally than conventional first-order or higher-order logics; they also empower programming languages where specifications may be incorporated into the type of programs, and well-typed programs are thus guaranteed to satisfy these specifications.

Students will learn at least one dependently-typed programming language in depth. The course will also cover associated foundations, including relevant type theories and the Curry-Howard correspondence, as well as useful patterns of formalising, programming, and proving in dependently-typed programming languages.

- Brief review of conventional logic, using CalcCheck
- Basic functional programming with pattern matching in Agda
- The Curry-Howard correspondence: Formulae as types, proofs as data
- Proving properties of functional programs
- Indexed datatypes
- Simple certified programs: Incorporating specifications into types
- Invariant-carrying datatypes
- Representing typed data: Expression languages, logics and programming languages
- Dependently-typed programming patterns: Universes, Views
- Category-theoretic abstractions as typed interfaces

**Lectures:**- Wednesdays and Fridays 12:00–13:30, for now on MS Teams

You are expected to exhibit honesty and use ethical behaviour in all aspects of the learning process. Academic credentials you earn are rooted in principles of honesty and academic integrity.

Academic dishonesty is to knowingly act or fail to act in a way that results or could result in unearned academic credit or advantage. This behaviour can result in serious consequences, e.g. the grade of zero on an assignment, loss of credit with a notation on the transcript (notation reads: “Grade of F assigned for academic dishonesty”), and/or suspension or expulsion from the university.

**It is your responsibility to understand what constitutes academic
dishonesty. **
For information on the various kinds of academic dishonesty
please refer to the Academic Integrity Policy, specifically Appendix 3,
located at
http://www.mcmaster.ca/academicintegrity

The following illustrates only three forms of academic dishonesty:

- Plagiarism, e.g. the submission of work that is not one's own or for which other credit has been obtained.
- Improper collaboration in group work.
- Copying or using unauthorized aids in tests and examinations.

“The Faculty of Engineering is concerned with ensuring an environment that is free of all adverse discrimination. If there is a problem that cannot be resolved by discussion among the persons concerned, individuals are reminded that they should contact the Department Chair, the Sexual Harassment Office or the Human Rights Consultant, as soon as possible.”

The instructor and university reserve the right to modify elements of the course during the term. The university may change the dates and deadlines for any or all courses in extreme circumstances. If either type of modification becomes necessary, reasonable notice and communication with the students will be given with explanation and the opportunity to comment on changes. It is the responsibility of the student to check their McMaster email and course websites weekly during the term and to note any changes.