Functional Programming for Logicians (2022)

January 2022, coordinated project in the Master of Logic at ILLC, University of Amsterdam. Instructor: Malvin Gattinger.

Schedule

Given Covid-19, this project will be fully online at least until 14 January. Later meetings might be hybrid. We will have lectures (L) and exercise (E) sessions.

DayWhe[n/re]WhatTopics
We 1209:00-11:00 zoom L1
.pdf
.lhs
Functions, Lists, Types, Propositional Logic
We 1213:00-15:00 gather E1 .pdf .lhs .hs
Th 1309:00-11:00 zoom L2
.pdf
.lhs
Type classes, QuickCheck, Modal Logic
Th 1313:00-15:00 gather E2 .pdf .lhs .hs
Fr 1409:00-11:00 zoom L3
.pdf
.lhs
Folds, Functors, Monads
Mo 1709:00-11:00 ??? L4
.pdf
.lhs
IO, Trees, Randomness, Projects
Mo 1713:00-15:00 ??? E3 .pdf .lhs .hs
We 1909:00-11:00 ??? L5 (Symbolic) Model Checking for (Dynamic) Epistemic Logic(s)
We 1913:00-15:00 ???E4
Fr 2109:00-11:00 ???L6 Beyond Haskell
Fr 2809:00-15:00 ??? Your Presentations
Fr 423:59 Report Deadline

You can also find the rooms here on DataNose. Note that DataNose might be wrong about which sessions are fully-online and which ones are hybrid!

Projects

During the remaining time after the lectures and exercise sessions you will work on your project in pairs (or groups of three). In week three you will give presentations.

You can find guidelines and a list of possible topics here. You can also come up with your own topic idea.

Links and References

Tools: Books: Additional Exercises: Hints and Tutorials:

Description

Functional Programming is a paradigm that focuses on functions instead of objects and states. Functional programs consist of definitions instead of instructions: We tell the compiler what we want to compute and not how to compute it.

Haskell is a lazy, strongly typed and purely functional programming language used in academia and industry. Based on lambda calculus and borrowing ideas from category theory, Haskell is an excellent tool for the mathematically inclined programmer. From a logician's point of view, the algebraic data types in Haskell make it very suitable to work with formal languages.

Depending on the background of the participants, this project will start with a fast introduction to Haskell and then focus on how it can be used as a research tool. We will focus on implementations of explicit and symbolic model checking for modal logics, but other topics from the whole Master of Logic spectrum are welcome.

At the end of this project you will understand the basics of Haskell: types, type classes, functors and monads; be able to implement model checking and other logic algorithms in Haskell; know how to use QuickCheck to test your code and to refute conjectures; have used Haskell to investigate a research question; be able to write well-documented programs.

Prerequisites

Basic knowledge of modal logic and set theory is expected. Courses on lambda calculus or category theory are a plus, but not necessary.

No programming experience is expected. On the contrary: If you have programmed in imperative languages before, be prepared to unlearn a few things.

You should bring a laptop to the exercise classes. A UNIX operating system (GNU/Linux or MacOS) is preferred. You should use an editor which works with the Haskell Language Server, for example VS Code or emacs. For your project you should also use git and the Haskell tool stack.

Sign-up

Sign-up is closed.