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. We then give a short introduction to the theory of Scott domains. After
that, we present the operational semantics and two versions of the denotational semantics for recursive programs. In that
context, we present the Scott induction rule for proving properties of
programs.
Organization
Winter Semester 2008.
·
Number: 326.00B
·
Title: Fixpoint
Theory of Functional Programs
·
Lecturer: Nikolaj Popov
·
Time: Tuesday
·
Place: K-223-B
·
Language: English
· First lecture: October 07
Registration
Please register for the course via the KUSSS system.
Contents
·
Computable, partial, total and recursive
functions. (Only introduction.)
·
Decidable and semidecidable
sets. The halting problem. (Only introduction.)
·
Compact, continuous, effective and recursive
operators. Knaster-Tarski, Myhill-Shepherdson
and Kleene theorems
·
Fixpoint induction.
Scott rule
·
Scott domains.
·
Syntax and operational semantics of recursive
programs.
·
Denotational semantics
of recursive programs. Call-by-value and call-by-name.
·
Equivalence of operational and denotational semantics.
·
Verification using fixpoint
induction.
[RISC-Linz] [University] [Search]