Table of Links 1 Introduction 1 Introduction 2 Course Structure and Conditions 2.1 Conditions 2.1 Conditions 2.2 Syllabus 2.2 Syllabus 3 Lectures 3 Lectures 4 Practical Part 4.1 Engagement Mechanisms 4.1 Engagement Mechanisms 4.2 Technical Setup and Automated Assessment 4.2 Technical Setup and Automated Assessment 4.3 Selected Exercises and Tools 4.3 Selected Exercises and Tools 5 Check Your Proof by Example 5 Check Your Proof by Example 6 Exams 6 Exams 7 Related Work 7 Related Work 8 Conclusion, Acknowledgements, and References 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 (∗) Introduction to functional programming Introduction to functional programming Basic Haskell: Bool, QuickCheck, Integer and Int, guarded equations, recursion on numbers Char, String, tuples 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 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 (∗) Proof by structural induction and computation induction on lists (∗) Type inference algorithm (∗) Type inference algorithm (∗) Higher-order functions: map, filter, foldr, λ-abstractions, extensionality, currying Higher-order functions: map, filter, foldr, λ-abstractions, extensionality, currying Typeclasses Typeclasses Algebraic datatypes and structural induction Algebraic datatypes and structural induction Concrete I/O without introducing monads (∗) Concrete I/O without introducing monads (∗) Modules: module syntax, data abstraction, correctness proofs Modules: module syntax, data abstraction, correctness proofs Case studies: Huffman codings, skew heaps Case studies: Huffman codings, skew heaps Lazy evaluation and infinite lists Lazy evaluation and infinite lists Complexity and optimisation Complexity and optimisation Monads (∗) 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 (kevin.kappelmann@tum.de);
(2) Jonas Radle, Department of Informatics, Technical University of Munich, Germany (raedle@in.tum.de);
(3) Lukas Stevens, Department of Informatics, Technical University of Munich, Germany (stevensl@in.tum.de). Authors: Authors: (1) Kevin Kappelmann, Department of Informatics, Technical University of Munich, Germany (kevin.kappelmann@tum.de); (2) Jonas Radle, Department of Informatics, Technical University of Munich, Germany (raedle@in.tum.de); (3) Lukas Stevens, Department of Informatics, Technical University of Munich, Germany (stevensl@in.tum.de). This paper is available on arxiv under CC BY 4.0 DEED license. This paper is available on arxiv under CC BY 4.0 DEED license. available on arxiv available on arxiv [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

Part of HackerNoon's growing list of open-source research papers, promoting free access to academic material.

Too Scared to Ask? How We Solved the #1 Problem with Large University Lectures

From Campus to Cloud: Our Journey Teaching Functional Programming to Thousands During a Pandemic

Pair Programming AI Agent 

Too Long; Didn't Read

Make resilience your competitive advantage

How Do You Teach I/O Before Monads? Inside a Radical Syllabus for a 1000-Student FP Course

About Author

Comments

TOPICS

THIS ARTICLE WAS FEATURED IN

Related Stories

Untitled Story

11 Proven Solutions to Common GitHub Copilot Problems

Automated Feedback Systems for Enhanced Tutor Training

Sequence Labeling for Automated Feedback in Tutor Training

GPT Models for Sequence Labeling: Prompt Engineering & Fine-tuning

Discussing GPT Models for Automated Explanatory Feedback in Tutor Training

11 Proven Solutions to Common GitHub Copilot Problems

Automated Feedback Systems for Enhanced Tutor Training

Sequence Labeling for Automated Feedback in Tutor Training

GPT Models for Sequence Labeling: Prompt Engineering & Fine-tuning

Discussing GPT Models for Automated Explanatory Feedback in Tutor Training

Light-Mode

Classic

Newspaper

Dark-Mode

Neon Noir

Minty

HN StartUps