Oris teme
Logic in computer science
This course exists at FMF under two different names: "Logika v računalništvu" and "Izbrana poglavja iz računalniške matematike" depending on your study programme. The course appears on the timetable under the latter name.
Please choose the time slot in which you will attend the exercise classes.
The exercise class can accommodate 15 students. Even if 15 places have been chosen, please still mark which of the two times you would be attending. We can use that overflow information to possibly argue for a bigger room.
Please answer this short poll through which we would like to assess the students' background and interests.
Resources
- Discord server devoted to the course. This is the easiest way to communicate with your teachers. Please use human-readable user names.
Installation instructions, exercises and other useful course materials.
Student projects
Project descriptions can be found at https://github.com/danelahman/lograc-2022/blob/main/projects/README.md.
Please try to organise yourselves into teams of two. Pairing up with somebody from your weekly exercise class group is also a good idea---then you can use the weekly 2hrs for working on the project together.
Of course, let the course organisers know if you have a topic in mind you would like to formalise in Agda that is not among the ones we have listed here.
Choose a date for your project presentation. Only one project member should do this. All presentations will take place between 14:00 and 17:00 on the chosen date.
Course materials
Prerequisites
Software
In this course we will be predominantly using the programming language and proof assistant Agda.
See the course's GitHub repository for instructions on how to install Agda and set up an interactive development environment for it.
Literature
We shall work through Part I to learn the basics of type theory and Agda. The remaining material will be useful to students who will work on programming-language related projects.
Caveat: Do not follow blindly the installation instructions given in the introduction, as they are fairly involved. We recommend instead that you use Visual Studio Code, which installs Agda automagically. (More instructions in the course's GitHub repository.)
- An excellent textbook that covers many topics on logic in computer science. We recommend it as a general background material. It will also prove useful for some student projects.