Hide menu

TDDD47 Programming Theory

Course information


Objectives | Prerequisites | Contents

Objectives

A natural question in programming is about the meaning of a given program. The meaning should be defined precisely in order to assure:
(1) human understanding of programs,
(2) compatibility of implementations: the program should execute in the same way regardless of the implementation used,
(3) correctness - the meaning of a program should conform to the intentions of the programmer.

The course gives an introduction to formal description techniques for defining semantics of programming languages, that is the meaning of each program of a given language. The objective is
(1) to give an insight into fundamental concepts of programming
(2) to discuss importance of the presented techniques for compiler construction
(3) to present techniques for proving correctness of programs.

Our intention is to give a solid overview of classical approaches to semantics of programming languages. We believe this knowledge is necessary for everybody interested in tools and/or formal methods dealing with program correctness.

Prerequisites

Familiarity with mathematical style of thinking. Courses on discrete mathematics and logic (TDDB90, TATM90 or equivalent). An advanced course on programming (like "Computer Languages and Programming" TDDB80).

Contents

Lectures (30h)

  • Introduction: motivations and survey of the course; abstract syntax (2h)
  • Part I. Description Formalisms (6 h)
    • Introduction to Standard ML
    • Lambda calculus
    • Transition systems with application to static typing
  • Part II. Operational Semantics (6h)
  • Part III. Denotational Semantics (8h)
    • Domains and semantic equations
    • Direct style semantics
    • Continuation semantics
  • Part IV. Axiomatic Semantics and Program Correctness (6h)
  • Closing discussion (2h)

Problem solving sessions (14h)

  • Tutorials (8h); two for Part II, one for Part III and one for Part IV.
  • Homework reporting sessions (6h)

Labs (14h)

  • ML (4h)
  • Operational semantics (4h)
  • Denotational semantics (4h)
  • (Reserve 2h)

Page responsible: Ulf Nilsson
Last updated: 2010-09-04