| Kursusnavn (dansk): | Domain Theory and Lambda Calculi |
| Kursusnavn (engelsk): | Domain Theory and Lambda Calculi |
| Semester: | Forår 2002 |
| Udbydes under: | cand.it., internet- og softwareteknologi (int) |
| Omfang i ECTS: | 7,50 |
| Kursussprog: | Engelsk |
| Kursushjemmeside: | https://learnit.itu.dk |
| Min. antal deltagere: | 0 |
| Forventet antal deltagere: | 0 |
| Maks. antal deltagere: | 0 |
| Formelle forudsætninger: | BSc in Computer Science or equivalent, mathematical maturity. |
| Læringsmål: |
During this course students will acquire the following skills:
- ability to explain the use of algebraic and topological structures in
the study of denotational semantics;
- ability to give denotational semantics to simple (imperative)
languages, and to prove correspondence between denotational and
operational semantics for those languages;
- ability to explain the difference between typed and untyped lambda
calculus;
- ability to explain the notion of models and ability to verify the model
property;
- experience with the language PCF and ability to apply
classical proof techniques;
- ability to solve simple domain equations.
|
| Fagligt indhold: | Denotational semantics aims to give mathematical meaning to
programming languages. Thus it provides rigorous definitions that
are implementation independent and which can be used for proving
properties of programs.
The goal of this course is to provide a systematic introduction to
the mathematical tools used in denotational semantics. In particular
we will study the syntax underlying modern programming
languages (lambda calculus and PCF), and semantics of those
languages (domains and cartesian closed categories).
We will work through the first seven chapters of the course
book. The reading will be eased by supplemental handouts. In detail
we will cover the following topics:
- domains, continuity, examples of denotational semantics;
- syntax of typed and untyped lambda calculus;
- models of the untyped lambda calculus (after Scott);
- models of the typed lambda calculus (cartesian closed categories);
- examples of models of the typed lambda calculus;
- the language PCF;
- domain equations.
|
| Læringsaktiviteter: | Lectures two hours each week, and tutorials/exercise classes three hours each week.
|
| Eksamensform og -beskrivelse: | X. experimental examination form (7-scale; external exam), 13-skala, Intern censur 4 hours written exam graded on the 13-scale. External censor. All written course material may be used at the exam.
Continuous assessment through submission of weekly coursework
exercises. Submission of at least 8 out of 11 weekly exercises and
performing at acceptable standards is prerequisite to sit the
exam. However, the final grade for this module is based solely on
the exam mark. External censor. It is allowed to use all written course-material to the exam.
|
| Litteratur udover forskningsartikler: | Amadio and Curien: "Domains and Lambda-Calculi".
Cambridge Tracts in Theoretical Computer Science 46,
Cambridge University Press, Cambridge 1998.
ISBN 0 521 62277 8 hardback
The book contains a wealth of information. However, the style is
fairly advanced and supplemental material will be provided.
|
| | |
Kursusoversigt