Funktionale Programmierung Functional Programming Ute Schmid Institut für Informatik, FB Mathematik-Informatik, Universität Osnabrück

Vorlesung im Wintersemester 2001/2002
(Lecture in winter term 01/02)

Kategorie: Informatik / Category: Computer Science

Course Language: material mostly English, presentation mostly German

Themen: Einführung in Konzepte der funktionalen Programmierung am Beispiel der Programmiersprache ML. Funktionen, Rekursion, Currying, Funktionen höherer Ordnung, Bindung, Evaluation, Lambda-Kalkül, Typ-Inferenz und Typ-Checking, Optimierung und Programmtransformation, Fixpunktsemantik, Theorembeweis und Verifikation.
Empf. Semester: 3. Sem. und höher (Voraussetzung Info A, hilfreich Info B und D)

Topics: Introduction to concepts of functional programming based on the programming language ML. Functions, recursion, currying, higher order functions (functionals), binding, evaluation, lambda calculus, type inferece and type checking, optimization and program transformation, fixpoint semantics, theorem proving and verification.
Proposed for students in 3rd or higher semester (prerequisite Info A, helpful Info B and D)

Hours and Contact

Online Information

Credits

Schedule and Syllabus

Assignements

• Lecture
  DI 12:30-14:00 in 31/322 and DO 14:15-15:45 in 31/322
  (orig. DI 14-16 in 31/449a and DO 12-14 in 31/E06)
• Tutorial
  MO 14-16 in 31/322 (first tutorial: 10/22)
  (orig. MO 14-16 in 31/449a)
• Contact: Ute Schmid, schmid@informatik.uni-osnabrueck.de
  Office Hours: MO 15:00-16:00 Uhr u.n.V. in 31/318
• Tutor: Marieke Rohde mrohde@uos.de

• Text Books:
  L. C. Paulson (1997). ML for the Working Programmer, 2nd Edition. Cambridge University Press.
  P. Pepper (2000). Funktionale Programmierung in Opal, ML, Haskell und Gofer. Springer.
  A. Field and P. Harrison (1988). Functional Programming. Addison-Wesley.
  [`Semesterapparat'/Literature]
• A Gentle Introduction to ML
• R. Harper, CMU: Programming in Standard ML
• Tutorial Papers for Functional Programming
• Functional Programming FAQ
• Functional Programming in the Real World
• The Journal of Functional Programming
• Free On-line Dictionary of Computing

• "Übungsschein": assignments or programming project.
• "Modul-Prüfung" (exam): Precondition is to get the "Übungsschein"; oral examination about the topics of the lecture.
• For cognitive science students this course is classified as "optional course in computer science" (12 credit points).

[Slides/Scriptum (pdf)] [Slides/Scriptum (ps)]

• 16.10.01: Introduction - Functional vs. "von-Neumann" Programming
• 18.10.01: FP Systems; evaluation and correctness of FP functions
• 23.10.01: Mathematical Foundations, Value Declarations in ML
• 25.10.01: Tuples, Records, and Datatype List
• 30.11.01: Evaluation, Recursion
• 01.11.01: Local Declarations and Modules
• 06.11.01: Polymorphic Type Checking and Type Inference
• 08.11.01: Unification of Type Expressions
• 13.11.01: Datatypes and Patterns
• 15.11.01: Datatype Exception, Recursive Datatypes, Tautology Checking
• 20.11.01: Anonymous Functions, Currying, Functionals
• 22.11.01: General Purpose Functionals
• 27.11.01: Infinite (Lazy) Lists
• 29.11.01: Reasoning about Functional Programs
• 04.12.01: Domain Theory and Fixpoint Semantics
• 06.12.01: Abstract Types and Functors
• 11.12.01: no class
• 13.12.01: Excursus: Program Synthesis
• 18.12.01: Modules
• 20.12.01: Realizing Dictionaries with Modules
• 08.01.02: Imperative Programming in ML

• 10.01.02: Elmar Ludwig - OO versus FP [Slides, pdf]
• 15.01.02: no class
• 17.01.02: no class
• 22.01.02: Kathrin Kröger & Jens Haubrich - Understanding Recursion [Slides I, htm] [Slides II, ps]
• 24.01.02: Martin Lindenthal - Erlang [Slides, html]
  [Slides TU-Berlin I, ps][Slides TU-Berlin II, ps] [Däcker Thesis, pdf] [Erlang Programming Rules, pdf] [Erlang Extensions 5.1,pdf] [Erlang,pdf] [SNMP, pdf] [Erlang Verification Tool]
• 28.01.02 (Monday!): Martin Beckmann - Functional Programming in Lisp vs. ML [Slides, pdf] [John McCarthy's Homepage]
• 29.01.02: Marieke Rohde - Recursive Program Schemes and Problem Solving[Slides, pdf] [Figures, jpg]
• 31.01.02: Bernd Pachur - Introduction to Theorem Proving [Slides, pdf]
• 04.02.02 (Monday!): David Soto - Example Implementation in Lisp (GPS) [Slides, htm]
• 05.02.02: Jens Waltermann - Theorem Proving with Isabelle [Paulson's proof of the Mutilated Chess Board problem, pdf][Isabelle] [Thousands of Problems for Theorem Provers]
• 07.02.02: Final Discussion

• [Moscow ML (preferred)] [Standard ML] [The Standard ML Basis Library]
• Start interpreter with mosml, quit with quit();, or, for Standard ML, start with sml, quit with <CTRL>-D.
• Load a program: use "myprog.ml";
• Each expression must be finished with semicolon (;)!
• sml automatically loads the needed structures from the standard library. For mosml, either all modules must be loaded in advance mosml -P full or the needed modules must be loaded explicely, e.g. load "Int";.
• For working on the assignments, the pool in room 31/433 can be used.

• [Assignment 1 (pdf)] due at 10/25 [Solution 1]
• [Assignment 2 (pdf)] due at 11/05 [Solution 2]
• [Assignment 3 (pdf)] due at 11/12 [Solution 3]
• [Assignment 4 (pdf)] due at 11/26 [Solution 4]
• [Assignment 5 (pdf)] due at 12/03 [Solution 5]
• [Assignment 6 (pdf)] due at 12/03 [Solution 6]
• [Assignment 7 (pdf)] due at 12/10 [Solution 7]
• [Assignment 8 (pdf)] due at 01/07 [Solution 8]

Top of page