Wednesday 12-15, Dan David 203

Instructor: Mooly Sagiv

TA:Oded Padon

This is an advanced course which covers many of the fundamental areas in the programming languages design and implementations. The topics include: operational and denotational program semantics, programming concepts such as higher order functions, lazy and eager evaluation, normal forms such as continuation passing style, polymorphism, type theory, dependent types, and monads. Techniques such as program verification, abstract interpretation, and partial evaluation. Applications such as domain specific programming languages.

Prerequisites: Compilation or programming languages course.

The grade of the course will be based on 10% course notes, 35% homework assignments, and 55% exam. There are two options for exam: home exam and class exam which is easier.

- Concepts in Programming Languages electronically available from the library 2183817
- Introduction to Haskel from Stanford
- Types and Programming Languages
- Foundations for Programming Languages
- Formal Semantics of Programming Language

- 25/10 Introduction
- 1/11 (13 because of Rabin's memorial) Introduction
to Haskell 1/11 (13 because of Rabin's memorial)

Class notes by Ori Barel and Maxim Finkel - 8/11 Lambda Calculus

Recitation

Class Notes by Andrey Leshenko Maxim Borin - 15/11 Operational Semantics

Class Notes by Idan Berkovits - 22/11 Denotational Semantics

Operational Semantics Recitation - 29/11 An Invited Lecture by Dr. Ori Lahav on Weak Memory Models
- 6/12 Axiomatic Semantics

Recitation: Denotational and Axiomatic Semantics - 13/12 Completeness of Axiomatic Semantics
- 20/12 Decidable Deductive Verification
- 28/12 Introduction to Static Analysis

Chaotic Iteration Python Code - 3/1 Theory of Chaotic Iteration "

- Assignment 1 Haskel due November 22
- Assignment 2: Lambda Calculus and Natural Operational Semantics November December 12
- Assignment 3: Due 3/1/2018
- Assignment 4: Due 24/1/2018

- Study the issue of filesystem verification using the articles from the FSCQ project
- Study models for weak memory as described by Ori Lahav
- Apply Dafny to verify an interesting program
- Apply Ivy to verify an interesting program.
- Study type safety of Java with generic
- Apply Astree to prove correctness of an interesting program

If your POWERPOINT does not show certain
mathematical characters use fonts in a zip file, by clicking
here.
Make sure to extract

them to the appropriate directory,

Alternatively, you can extract them anywhere, and install them via the control panel