Programming for DEL Tutorial

• It is a good idea to use your own laptop.
• If you use your own laptop, make sure the Haskell platform is installed on it. See platform.

Tutorial Topics

• Logic and Functional Programming (based on my talk "Logic, Languages and Programming" for the Minor Programming). Code for this: LLP.hs.
• Representing Relations (based on my technical report "Relations, Equivalences, Partitions", Feb 2014). Code for this: EREL.hs.
• DEMO-S5: Explanation of the workings of the DEMO-S5 model checker. Code for this: DEMO-S5.hs.
• Model Checking for Probabilistic DEL: Explanation of the workings of the PRODEMO model checker. Code for this: PRODEMO.hs.
• Model Checking Cryptographic protocols: demo of a prototype implementation of Register-DEL, by Malvin Gattinger.
• If there is time we can also discuss the way forward: what kind of features do we want to see in model checking tools for DEL?

Course material

Kees Doets and Jan van Eijck, The Haskell Road to Logic, Maths and Programming, College Publications, second edition (2012). See here.

Further course material will be distributed in the course of the day.