Table of Links
1 Introduction
2 Course Structure and Conditions
2.1 Conditions
2.2 Syllabus
3 Lectures
4 Practical Part
4.1 Engagement Mechanisms
4.2 Technical Setup and Automated Assessment
4.3 Selected Exercises and Tools
5 Check Your Proof by Example
6 Exams
7 Related Work
8 Conclusion, Acknowledgements, and References
2 Course Structure and Conditions
2.1 Conditions
The 5 ECTS[2] course was mandatory for computer science undergraduates in their third semester and an elective for other related degrees such as games engineering or information systems. All students studied Java in their first semester and had taken courses on algorithms and data structures, discrete mathematics, and linear algebra. The course ran for 14 weeks with one 90-minute lecture, one 90-minute tutorial, and one exercise sheet each week.
1057 students registered for the first iteration[3] that took place on campus in winter semester 2019 (WS19) and 1031 for the second iteration[4] in winter semester 2020 (WS20), taking place in virtual space due to the COVID-19 pandemic.
Both iterations were organised by the lecturer, Tobias Nipkow, and the authors of this paper. The former designed the lecture material, created the slides[5], and delivered the lectures. The others took care of the practical and organisational part of the course. All gained valuable experience in running an online course on the theory of computation for 1071 students in summer semester 2020. Finally, Manuel Eberl had the honour of assisting us with the weekly programming competition (see Section 4.1).
Needless to say, running tutorials for more than 1000 students each semester on our own is impossible. We were further assisted by 13 student assistants in WS19 and 22 student assistants in WS20. In WS19, their primary job was to run the tutorials and provide feedback for homework submissions (e.g. code quality). However, it became clear to us that this manual feedback is not effective and that their time is better spent creating engaging exercises (see Section 4.1). On average, each assistant worked 10 hours per week, spending 4 hours on running tutorials and the remaining 6 hours preparing themselves for the tutorials, grading student submissions, and implementing new exercises for students.
2.2 Syllabus
The course deals with the basics of functional programming and the verification of functional programs. Most parts of the course could be done using any functional language. We chose Haskell because of its simple syntax, large user community, and good testing facilities (in particular QuickCheck). The syllabus stayed close to the one presented in [4]. The changes are the omission of the parser case study, the rigorous introduction of computation induction and type inference, and the decision to split off I/O from monads and introduce it earlier. The last is done in an effort to convince students more quickly that pure functional languages can be practical and deal with side effects. For ease of reference, we list the syllabus below. New or modified topics are marked (∗):
-
Introduction to functional programming
-
Basic Haskell: Bool, QuickCheck, Integer and Int, guarded equations, recursion on numbers Char, String, tuples
-
List comprehension, polymorphism, a glimpse of the Prelude, basic typeclasses (Num, Eq, Ord), pattern matching, recursion on lists (including accumulating parameters), scoping by example
-
Proof by structural induction and computation induction on lists (∗)
-
Type inference algorithm (∗)
-
Higher-order functions: map, filter, foldr, λ-abstractions, extensionality, currying
-
Typeclasses
-
Algebraic datatypes and structural induction
-
Concrete I/O without introducing monads (∗)
-
Modules: module syntax, data abstraction, correctness proofs
-
Case studies: Huffman codings, skew heaps
-
Lazy evaluation and infinite lists
-
Complexity and optimisation
-
Monads (∗)
Concepts are introduced in small, self-contained steps. Characteristic features of functional programming languages such as higher-order functions and algebraic data types are only introduced midway through the course. This makes the design of interesting practical tasks harder but ensures that students are not overwhelmed by the diversity of new principles that are not part of introductory imperative programming courses. In general, the course progresses from ideas close to what is known from imperative languages (e.g. boolean conditions, recursion on numbers, auxiliary functions, etc.) to simple applications of new concepts (e.g. recursion and induction on lists) to generalised new concepts (e.g. algebraic data types and structural induction).
Authors:
(1) Kevin Kappelmann, Department of Informatics, Technical University of Munich, Germany ([email protected]);
(2) Jonas Radle, Department of Informatics, Technical University of Munich, Germany ([email protected]);
(3) Lukas Stevens, Department of Informatics, Technical University of Munich, Germany ([email protected]).
[2] European Credit Transfer System; one ECTS credit equals 30 hours of work
[3] https://www21.in.tum.de/teaching/fpv/WS19/ (website – except “Wettbewerb” – German; course material English)
[4] https://www21.in.tum.de/teaching/fpv/WS20/ (English)
[5] https://www21.in.tum.de/teaching/fpv/WS20/assets/slides.pdf