Introduction to Informatics 2

Among others, the module IN0003 is concerned with the following topics:
- Correctness of imperative programs
++ Verification according to Floyd or Hoare
++ Termination
++ Procedures
- Basic concepts of functional programming
++ Values, variables, functions
++ Data++structures, pattern matching
++ Higher order functions
++ Polymorphic types
++ Programming in the large: Structures and Functors
++ Correctness of functional programs
+++ Semantics of functional programs
+++ Verification of functional programs

After successful completion of the module, participants understand the key concepts of functional programming languages. They are able to solve well presented tasks in a functional programming language. Therefore, they are able to acquire programming skills on their own also in further functional programming languages. They also are familiar with the most important techniques for the verification of imperative and functional programming language and can apply them to simple programs.

IN0001 Introduction to Informatics

By means of a presentation, either by slides or whiteboard, the lecture transports the concepts of verification and the programming language and illustrates them by examples.
Accompanying assignments for individual study deepen the understanding of the concepts explained in the lecture, and train students to apply these to the verification of small programs and to master programming in the given programming language.

Slide show, blackboard, possibly online programming and/or animations

Guy Cousineau und Michel Mauny, The Functional Approach to Programming, Cambridge University Press, Cambridge, 1998
Apt, Olderog: Programm-Verifikation. Springer 1991
Gerd Smolka: Programmierung - eine Einführung in die Informatik mit Standard ML. Oldenburg, 2007
Simon Tompson: Haskell: the Craft of Functional Programming. Addison-Wesley, 2011

The exam takes the form of a 120 minutes written test. Small programming tasks allow to assess whether the students master a functional programming language and are able to realize small implementation problems. By inferring simple invariants they demonstrate that they have understood the principles of program verification and are able to apply these.
The successful completion of homework asignments may contribute to the grade as a bonus. The exact details for this are announced timely at the begin of the lecture.