Functional Programming and Verification

Chair for Logic and Verification

Overview

The slides and exercise sheets will be offered in English. Moreover, some tutorials will be held in English. The exam will be in English. The lectures will be livestreamed in German including moderated live Q&As using Tweedback. The Tweedback link will be updated each week in below table.

Professor Prof. Tobias Nipkow
Time and Place Livestream on Friday 8.30-10.00am (Tweedback link 12.02: https://tum.tweedback.de/p186)
First Lecture 2020-11-06
Language German (English slides and tutorials available)
TUMonline IN0003
Moodle https://www.moodle.tum.de/course/view.php?idnumber=950496106
Submission System Artemis
Discussion Forum Zulip (subscribe to “FPV-*” streams)
Tutorial Organisors Jonas Rädle, Lukas Stevens and Kevin Kappelmann

Questions regarding the lecture and exercises can be discussed on Zulip. You are not allowed to share and discuss homework solutions before the submission deadline. Doing so will result in a ban from the grading bonus.

The organisors can be contacted at fpv@in.tum.de. Please only do so in special cases and try to resolve your questions on Zulip first.

Content

In this course, students get to know the key concepts of functional programming languages. They will solve well presented tasks in a functional programming language (Haskell). They will also be equipped with the most important techniques for the verification of functional programming languages (inductive proofs) and will be able to apply them to simple programs in a formal matter. Moreover, as non-functional programming languages increasingly implement functional paradigms, concepts taught in this course will largely be applicable to other programming languages as well, increasing code readability, stability, and correctness.

Lecture Material

Haskell

Use the installation instructions to set up your programming environment for the tutorials and homeworks. If you face any problems, you can ask for help at this BBB room on Friday, 06.11.2020 at 14.00–15.00 and 17.00–18.00.

Official Sources: Website, books, tutorials, and language definition.

Literature

The lecture is guided by - Simon Thompson. Haskell - The Craft of Functional Programming. Addison-Wesley.

A more compact, recommended introduction is - Graham Hutton. Programming in Haskell. Cambridge University Press.

Functional Programming in Industry

Functional programming is steadily increasing its popularity, and even non-functional programming languages increasingly implement functional paradigms. Functional programming languages are known to be less error-prone than imperative langauges with side-effects. As an example, Jane Street Capital, an international finance institution, relies on the functional programming language OCaml. Reports can be found here.

There are many success stories of Haskell [1] and OCaml [2] in industry. Here are some more examples for industrial functional programming reports: Credit Suisse, Twitter, Naughty Dog Inc., Trifork, Citrix, S&P Capital IQ, Verizon, Pfizer, and Facebook.

Even some local companies, like our past FPV-competition sponsors active-group, QAware, and TNG, supporting the Munich Haskell hackathon MuniHac, find great interest in experienced functional programmers or even base all their business software on functional programming languages.