About the course
Contents
About the course¶
These are the lecture notes for the course Logika v računalništvu 2021/22 (doubling as “Izbrana poglavja iz računalniške matematike”) at the Faculty of Mathematics and Physics, University of Ljubljana.
These notes are not a complete resource but rather just a scaffolding for the live lectures. Please consult the video recordings for a complete record.
Prerequisites¶
We assume general knowledge of undergraduate mathematics and familiarity with programming. We shall use the following technology:
The proof assistant Agda
Revision constrol with
gitand GitHubIn addition, depending on your project, you might use other tools, such as Lean and F*.
In the first lecture you will find instructions for installing Agda, and the rest you need not worry about yet.
Those who are not yet familiar with git will have to put in a little bit of extra work in the beginning to learn its basic usage, as we shall rely heavily on it. Do not worry, we can point you to a number of good tutorials and documentation, and we are always here to answer questions. We encourage cooperation between students. If you have experience with git and Visual Studio Code, please offer help to those who are not.
We will learn Agda and the other tools from scratch. No familiarity with these is assumed.
Course requirements¶
To complete the course, you need to complete and present a project. We anticipate that all students will complete and present their work by the end of the classes.
The projects will be determined and assigned at a later time. They will cover topics in formalization of mathematics, formalization of programming languages, and verification of implementation of data structures and algorithms. If you have a particular interest in one of these or a relevant related project, let us know so that we may find a project that suits your interests.
Depending on the number of students attending the course, we may form project teams of size two.
Schedule¶
Lectures: Thursday 13:00–16:00, room 3.07
Exercises:
Group 1: Friday 10:00–12:00, room 3.11
Group 2: Monday 12:00–14:00, room 3.12
Please choose your exercise group if you have not done so yet.
Resources¶
Course material¶
The official course page
Video recordings of lectures
We have a Discord server whose invitation link is available on the course page
Course repository (a link will be provided soon)
Supplementary reading material¶
Programming Language Foundations in Agda by Phil Wadler: Part 1 covers in detail much of what we will learn. The rest of the notes develop the theory of programming languages in Agda and will be of interest to the students who are interested in the topic.
Introduction to Univalent Foundations of Mathematics with Agda by Martín Escardó: Chapter 2 presents the basics of type theory in Agda, and the rest is an introduction to Univalent foundations of mathematics (also known as homotopy type theory).
Technical resources and documentation¶
Proof assistants questions & answers StackExchange site
Lean proof assistant and the Lean community page
F* language for program verification