Programming Languages Semantics with Applications

Instructor: Shmuel (Mooly) Sagiv
Lecture: Sunday 14-17, Schriber 8
Prerequisites: Compilers

Motivation

While the syntax of a programming language is always formally specified, the equally important aspect of defining its meaning is often left to natural language which is ambiguous and leaves questions open. In order to understand the inherent properties of a language (e.g. for constructing a compiler), we should have a deeper understanding. The goal of formal semantics is to reveal the essence of a language beneath its syntactic surface.

This is the first time that this course is provided. In the first part of the course we will describe the basic techniques used for defining semantics. In the second part of the course we plan to cover applications of program semantics including program verification, program analysis, and type checking.

Important Message

If your POWER POINT does not show certain mathematical characters use fonts in a zip file, by clicking here. Make sure to extract them to the appropriate directory, that is
Fonts you can extract them anywhere, and install them via the control panel

Course Requirements

Bibliography

Schedule

  1. Sunday May 12 Overview
    Class notes by Daphna Amit and Inon Peled
  2. Friday 11:10-13:10 May 16 Holtzblat 07 Operational Semantics PPT PDF
    Class Notes by Natalia Cherniavsky and Uri Israeli
  3. May 18 Denotational Semantics revised PPT revised PDF
    Class Notes by Tom Yam and Michael Kuperstein
    Class Notes by Maor Hizkiev, Eyal Altshuler and Ariel Jarovsky
  4. May 25 Axiomatic Semantics: PPT PDF
    Class Notes by Stas Levin and Shay Erov
  5. June 17 Axiomatic Semantics of Parallel Programs: PPT PDF
    Class Notes by Udi Ben-Porat & Michal Segalov
  6. June 22: Rely/Guarantee Reasoning: PPT PDF
    Class notes by Opher Lieber and Omer Ran
    Bibliography by Clif Jones
    An application to proving Linearizability
  7. June 29: Local Reasoning:
    PPT PDF
    Class notes by Roman Manevich and Ohad Shacham
    BI as an Assertion Language for Mutable Data Structures
    Peter O'Hearn's Page on Separation Logic
  8. July 6: Type Checking:
    PPT PDF
    Class notes by Lahav Yeffet and Ori Folger

Homework Assignments

  1. Assignment 1: Due June 1st
  2. Assignment 2: Due July 14th
  3. Assignment 3: Due August 1st
  4. Assignment 4: Due August 18th Only for those who did not prepare class notes

For further information Email: msagiv@post.tau.ac.il