This course is an introduction to logic and foundations from both a modern point of view (based on type theory and its relations to topology) as well as in the traditional formulation based on first-order logic.
Most of the material will be developed using the dependently typed language Idris. Connections with programming in functional languages and the use of dependent type theory to integrate computations and proofs will be explored.
The code for this course, including the live code in lectures is available in the repository (the octocat on the top right corner also links to this).
The main aim of this course is to give a self-contained exposition of the (topological) foundations of mathematics and computation known as Homotopy Type Theory. These are foundations that are close to real-life mathematics, allow an integration of programs and proofs, and have deep connection with .
The only background assumed is some basic mathematics, in particular being comfortable with proofs and with the concept of continuity (at least over real numbers). Some familiarity with programming will be helpful, but mainly a willingness to learn and write code. In particular no familiarity with Idris or functional programming, or with formal logic, is assumed.
Note that the topic of this course is not a mature subject. In particular there is no book at this level. This will require some maturity and open-mindedness from the students.
To get a head-start on the course, 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). You may also wish to get familiar with the version control system
At least 50% of the grade will be based on assignments and projects, which will be in
Idris. Please e-mail your assignments to email@example.com with "LTS2019" in the subject. The submissions will be added to the repository the day after the due date, and no late submissions will be accepted.