RISC JKU

Fixpoint Theory of Functional Programs

Short Description

In this course we study the fixpoint theory of programs, developed by D. Scott, and we consider the semantics of programs defined as least fixpoints of recursive operators. The topics we will cover include: Computable, partial, total and recursive functions; Decidable and semidecidable sets. The halting problem; Compact, continuous, effective and recursive operators; Knaster-Tarski, Myhill-Shepherdson and Kleene theorems; Fixpoint induction, Scott induction rule for proving properties of programs.

This course is intended for students of mathematics or computer science who are interested on the theoretical foundations of computer science. There is no particular prerequisite for the course.

Organization

Winter Semester 2010.

Registration

Please register for the course via the KUSSS system.


Maintained by Nikolaj Popov