Lecture notes
Most of the lectures are based on a text book while others follow the documents below.
Text book
Hanne Riis Nielson, Flemming Nielson: Semantics with Applications: An Appetizer, Springer, 2007. It can bought for less than 300 SEK from Swedish net sellers. It is possible to read the book online at Springer (maybe with restrictions).
Lambda calculus
Lambda calculus is a very small language used to describe computations. It is the basis for all functional programming languages and it sometimes used to define the semantics for all kinds of programming languages.
Representation
This document describes the difference between concrete representation using grammars and abstract representation using data types. It should familiar to those who have followed EDAF10 (OMD with discrete structures) or EDA180 (Compiler construction).
Induction
Structural induction is an important tool to prove properties of trees, such as abstract representations of programs. It is equivalent to standard mathematical induction over natural numbers.
Deduction
In axiomatic semantics (for programming languages) one build proof trees. This document applies the same technique to language of statement and predicate logic. Again, this has been discussed in EDAF10 as Natural deduction.
Domain theory
This theory is about the meaning of recursive definitions and the solution of an important class of system of equations where the unknowns are sets, functions, data types etc.
Prolog
Prolog is a programming language based on predicate logic. We introduce the language and study the execution model.
Haskell
Haskell is a functional language used in the course EDAN40 (Functional programming). It is suitable for implementing programming language semantics as executable programs, and of course, an excellent example of how Lambda calculus can be turned into a programming language.
Natural numbers
This is about the semantics of natural numbers as given by the axioms of Peano.
SECD
This document describes an execution model for Lambda calculus, the SECD machine.
Attribute grammars
This another way to define the semantics of programming languauges. It has been generalized by Görel Hedin and is used an in JastAdd.
pdf
Dependent types
A dependent type is a type that depends on a value, see
Norell: pdf
Bove, Dybjer:pdf
Barendregt: pdf