## Contents

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 git and GitHub

• In 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.