lu.se

Denna sida på svenska This page in English

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.

pdf

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).

pdf

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.

pdf

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.

pdf

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.

pdf

Prolog

Prolog is a programming language based on predicate logic. We introduce the language and study the execution model.

pdf

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.

pdf

Natural numbers

This is about the semantics of natural numbers as given by the axioms of Peano.

pdf

SECD

This document describes an execution model for Lambda calculus, the SECD machine.

pdf

 

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

Sidansvarig: