June 2018, coordinated project in the Master of Logic at ILLC, University of Amsterdam.

Instructors: Malvin Gattinger and Jana Wagemaker.

Day | Time | Room | What | Planned Topics |
---|---|---|---|---|

Mo 4 | 10:00-12:00 | F3.20 | Lect. | Functions, Lists, Types L1: .pdf .lhs |

Mo 4 | 14:00-16:00 | F1.15 | Ex. | E1: .pdf .lhs |

Tu 5 | 10:00-12:00 | F3.20 | Lect. | Type classes, QuickCheck, Modal Logic L2: .pdf .lhs |

Tu 5 | 13:00-15:00 | F3.20 | Ex. | E2: .pdf .lhs |

We 6 | 10:00-12:00 | F1.15 | Lect. | Functors, Monads, IO L3: .pdf .lhs |

Th 7 | 10:00-12:00 | F1.15 | Lect. | IO, Randomness, Trees, Practical Stuff L4: .pdf .lhs |

Th 7 | 14:00-15:30 | F1.15 | Ex. | E3: .pdf .lhs |

Fr 8 | 10:00-12:00 | F1.15 | Lect. | (Symbolic) Model Checking for (Dynamic) Epistemic Logic(s) L5: .pdf |

Fr 8 | 14:00-16:00 | F1.15 | Ex. | E4: .pdf .lhs |

Fr 15 | 09:00-11:00 | F1.15 | Your Presentations | |

Fr 22 | 18:00 | Optional Work-In-Progress Deadline | ||

Fr 29 | 15:00 | Report Deadline |

The first week will consist of daily lectures and exercise sessions. During the remaining time you will work on your own or in pairs, on a specific research topic.

Here you can find a list of topics, but you can also come up with your own. Please send us an email by Sunday 10th of June what you would like to work on.At the end of the second week you will give a short presentation about your project and at the end of the month you will submit a report in literate programming style for which you can use this template.

For grading criteria, see the last slide of L5.pdf. It is not mandatory, but a good idea to send us a work-in-progress version of your report to get some feedback, around June 18–22.

- The Haskell Tool Stack
- Hoogle for stackage lts-11.11
- Haskell on exercism.io
- Pandoc can convert lhs to pdf files (and a lot more).

- Miran Lipovača: Learn You a Haskell for Great Good!
- Kees Doets & Jan van Eijck: The Haskell Road to Logic, Maths and Programming
- Bryan O'Sullivan, Don Stewart, and John Goerzen: Real World Haskell

- Ian: Good Haskell Style
- Stephen Diehl: What I Wish I Knew When Learning Haskell

- Michael Snoyman: Primitive Haskell
- Haskell Wiki: Ternary Operator
- Malvin Gattinger: A Model Checker for the Hardest Logic Puzzle Ever
- Malvin Gattinger: New Directions in Model Checking Dynamic Epistemic Logic

Functional Programming is a paradigm that focuses on mathematical definitions 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 that is getting more and more popular in academia and different industries. Based on lambda calculus and borrowing some ideas from category theory, Haskell is an excellent tool for the mathematically inclined programmer. From a logician's point of view, its data types make it very natural 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, including for example:

- Natural Logic
- Sudoku Solving
- Theorem Proving
- Binary Decision Diagrams
- Haskell and Category Theory
- Modular Arithmetic and Public Key Cryptography

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 literate programs

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 coded in imperative languages before, you should be prepared to unlearn a few things.

You should have a laptop for the exercise classes. A UNIX operating system (GNU/Linux or MacOS) is preferred. You should use a good text editor, for example vim, emacs (plus intero), atom (plus packages) or sublime. Similarly, it would be good if you are already familiar with git. We use the Haskell tool stack.