uva.nl
ILLC

Master of Logic / ILLC

Submit Coordinated Project

1st Semester 2021/22: Functional Programming for Logicians

Instructors
Malvin Gattinger
ECTS
6
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.

 

To sign up for this project, please send an email to with

  • - your full name,
  • - whether you have programmed before and in which languages, and
  • - other topics you are interested in.

More information will be available during the project at https://malv.in/2022/funcproglog.

 

Organisation

In the first two weeks we will have lectures and exercise sessions. During the remaining time you will work on your own or in pairs, on a specific research topic.

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, you should be prepared to unlearn a few things.

Assessment
  • presentation at the end of week 3
  • report and software to be submitted at the end of week 4
References

Miran Lipovača: Learn You a Haskell for Great Good! http://learnyouahaskell.com/

Malvin Gattinger: New Directions in Model Checking Dynamic Epistemic Logic https://malv.in/phdthesis/


Back