Formal Semantics of Programming Languages (SS 2009)

Section outline

• Select section General

  General

  Collapse all Expand all

  Formal Semantics of Programming Languages (326.027, SS 2009)
  
  Time: Friday, 8:30-10:00, HS 13.
  Start: March 6, 2009.
  
  While the syntax of a programming language is always formally specified, the equally important aspect of definining its meaning is often left to natural language which is ambiguous and leaves many questions open. In order to understand the inherent properties of a language (e.g. for constructing a compiler), we should have a deeper understanding.
  

  This course presents some major methods for defining the meaning of programming languages (and thus programs) and discusses their relationship:

  Denotational Semantics

  A programming language is defined by a valuation function that maps a program into a mathematical object which is considered as its meaning.

  Operational Semantics

  A programming language is defined by reduction rules that describe how the initial state of a program is transformed step by step into the terminal state.
  

  Axiomatic Semantics

  A programming language is defined by correctness assertions that describe how to draw conclusions about the input/output interface of a program.
  

  The participants are expected to elaborate small exercises which will be used for grading (there will be no final exam).

  ---

  To take part in the course, you have to enrol in the KUSSS system. If you also login in Moodle and register as a course participant, you will receive per email all messages posted in the News forum.
  
  

  • Select activity Literature

    

    Literature Page
  • Select activity News forum

    

    News forum
• Select section Topic 1

  Topic 1

  Denotational Semantics (Part 1)

  • Select activity Denotational Semantics

    

    Denotational Semantics File
  • Select activity Syntax

    

    Syntax File
  • Select activity Figures (protected)

    

    Figures (protected) URL
  • Select activity Sets, Functions, Domains

    

    Sets, Functions, Domains File
  • Select activity Semantic Algebras

    

    Semantic Algebras File
  • Select activity Basic Structure of Denotational Definitions

    

    Basic Structure of Denotational Definitions File
  • Select activity Figures (protected)

    

    Figures (protected) URL
  • Select activity Imperative Languages 1

    

    Imperative Languages 1 File
  • Select activity Figures (protected)

    

    Figures (protected) URL
• Select section Topic 2

  Topic 2

  Operational Semantics

  • Select activity Introduction (protected)

    

    Introduction (protected) URL
  • Select activity Equivalence to Denotational Semantics (protected)

    

    Equivalence to Denotational Semantics (protected) URL
• Select section Topic 3

  Topic 3

  Denotational Semantics (Part 2)

  • Select activity Domain Theory 1

    

    Domain Theory 1 File
  • Select activity Domain Theory 2 (protected)

    

    Domain Theory 2 (protected) URL
  • Select activity Imperative Languages 2

    

    Imperative Languages 2 File
  • Select activity Figures (protected)

    

    Figures (protected) URL
• Select section Topic 4

  Topic 4

  Languages with Contexts

  • Select activity Languages with Contexts 1: A Block-Structured Language

    

    Languages with Contexts 1: A Block-Structured Language File
  • Select activity Figures (protected)

    

    Figures (protected) URL
  • Select activity Languages with Contexts 2: An Applicative Language

    

    Languages with Contexts 2: An Applicative Language File
  • Select activity Figures (protected)

    

    Figures (protected) URL
  • Select activity Languages with Contexts 3: Compound Data Structures

    

    Languages with Contexts 3: Compound Data Structures File
• Select section Topic 5

  Topic 5

  Axiomatic Semantics

  • Select activity Axiomatic Semantics (protected)

    

    Axiomatic Semantics (protected) URL
• Select section Topic 6

  Topic 6

  Exercises
  

  4 exercises will be handed out.
  

  • Select activity Exercise 1 (April 6)

    

    Exercise 1 (April 6) Assignment
  • Select activity Exercise 2 (May 25)

    

    Exercise 2 (May 25) Assignment
  • Select activity Exercise 3 (June 29)

    

    Exercise 3 (June 29) Assignment
  • Select activity Exercise 4 (July 13)

    

    Exercise 4 (July 13) Assignment