Syllabus 2008/2009 EDA145

Syllabus academic year 2008/2009
(Created 2008-07-17.)

PROGRAMMING LANGUAGE THEORY

EDA145

Higher education credits: 7,5. Grading scale: TH. Level: A (Second level). Language of instruction: The course will be given in Swedish. Optional for: D3, D3ps, E3, E3ps, F3, Pi4. Course coordinator: Lennart Andersson, Lennart.Andersson@cs.lth.se, Inst f datavetenskap. Prerequisites: EDA027 Algorithms and Data Structures or EDAA01 Programming - Second Course. FMA410 Calculus in One Variable, FMA420/FMA425 Linear Algebra and FMA430/FMA435 Calculus in Several Variables. The course might be cancelled if the numer of applicants is less than 20. Assessment: Written examination. The students are expected to present solutions to selected problems at seminars. Further information: The course is given periodically. It is planned to be given every second year (odd years) during spring term. The course might be cancelled if there are less than 20 participants. Home page: http://www.cs.lth.se/EDA145.

Aim
The course will give a qualified perspective on the semantics of programming languages and ability to read and understand scientific papers in a wider field than the course contents.

Knowledge and understanding
For a passing grade the student must

be able to understand the semantics of program constructs given as formal operational, axiomatic, and denotational semantics.
be able to understand execution models for functional and logic programming languages.

Skills and abilities
For a passing grade the student must

be able to specify formal semantics given as informal descriptions.
be able to interpret recursive definitions using least fixed points.
be able to make computations using lambda calculus and combinatory logic.
be able to construct programs for type deduction and unification.
be able to prove program properties such as correctness and equivalence.

Judgement and approach
For a passing grade the student must

be able to value program constructs based on their formal semantic descriptions.

Contents
Syntax of programming languages and abstract representation of programs. Operational, axiomatic, and denotational semantics. Proofs of program properties. Domain theory and semantics of recursive definitions. Lambda calculus and combinatory logic. Execution models for programming languages. Unification and type deduction.

Literature
Nielson, H R, Nielson, F: Semantics with Applications: An Appetizer.
Publishing information is not yet available.
Andersson, L: Lecture notes. Datavetenskap 2006.