SEMANTICS (2016)

ECTS credits: 5 ECTS

Course parameters:
Language: English
Level of course: PhD course
Time of year: Q1, fall 2016
No. of contact hours/hours in total incl. preparation, assignment(s) or the like: 25/143
Capacity limits: max. 8 participants

Objectives of the course:
The course takes a pragmatic and research-based approach to studying semantics of formal languages typically used for programming or specification. The course material consists of a collection of books from the standard literature and research articles on the subject representing a common mixture that would be encountered in literature research on the subject. As such the course has two major objectives: (1) to familiarise the students with different notions of formal semantics and (2) to approach a new subject, in this case “semantics”, systematically. The course complements existing courses on compiler construction, formal verification and formal specification.

Learning outcomes and competences:
At the end of the course, the student should be able to:

  • Specify common concepts of formal languages in the discussed semantic paradigms
  • Explain and compare the different semantic paradigms
  • Reason about syntax, meaning and correctness
  • Acquire a new subject and specialisations from standard literature and research articles
  • Present and explain the acquired material to others

Compulsory programme:
None

Course contents:
The course will be held in seminar style as a series of student presentations. The course will review three major semantic paradigms: operational semantics, axiomatic semantics and denotational semantics. Common features of formal languages will be treated in a combination of different semantics: assignment, sequential composition, conditional statements, loops, procedures, recursion, non-determinism, and concurrency. Mathematical proofs will be used to establish relationships between the different semantics.

Prerequisites:
Some familiarity with formal languages and discrete mathematics.

Name of lecturers: 
Stefan Hallerstede and Peter Gorm Larsen

Type of course/teaching methods:
Seminar (3h/week)

Literature:
[1]   K. R. Apt, F. S. de Boer, E.-R. Olderog. Verification of Sequential and Concurrent Programs, Third Edition, Springer, 2009

[2]   E. W. Dijkstra, C. S. Scholten. Predicate Calculus and Program Semantics. Springer, 1990.

[3]   E. C. R. Hehner. A Practical Theory of Programming. Springer, 1993.

[4]   H. R. Nielson, F. Nielson. Semantics with Applications – An Appetizer. Springer, 2007.

[5]   D. A. Schmidt. Denotational Semantics. Allyn and Bacon, 1986.

[6]   G. Winskel. The Formal Semantics of Programming Languages – An Introduction. MIT, 1993.

Course homepage:
None

Course assessment:
Each student has to give two presentations on language semantics, typically, one from a textbook and one from a research article. Furthermore, a common project of all participating students on describing the semantics of a formal language supplied by course leaders has to be worked out. The expected result from this activity is a corresponding technical report.

Provider:
Department of Engineering, Aarhus University

Special comments on this course:
None

Time:
TBD

Place:
Aarhus University, Department of Engineering, Finlandsgade 22, 8200 Aarhus N, Room: TBD

Registration:
Deadline for registration is 1 August 2016. Information regarding admission will be sent out no later than 8 August 2016.

 

For registration: send e-mail to sha@eng.au.dk detailing your prerequisites, in particular.

If you have any questions, please contact Stefan Hallerstede, e-mail: sha@eng.au.dk

Comments on content: 
Revised 14.07.2016