(Created 2010-07-25.)

PROGRAMMING LANGUAGE THEORY | 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. Springer 2007. ISBN 978-1-84628-691-9

Andersson, L: Lecture notes. Datavetenskap.