Students enrolled in this class are expected to check this web page regularly. Lecture notes and important other material will be posted here.
Course Description
CS522 is an advanced course on semantics of programming languages. Various semantic approaches and related aspects will be defined and investigated. Executable semantics of various programming languages and paradigms will be discussed, together with major theoretical models.
 Meetings: Tu/Th 9:30  10:45, 1103 Siebel Center
 Professor: Grigore Rosu (Office: SC 2110, WWW: http://fsl.cs.illinois.edu/grosu, Email: grosu@illinois.edu)
 Office hours: By appointment, very flexible (held by Grigore Rosu in SC 2110)
Piazza Page
CS522 Piazza Page
Lecture Notes, Useful Material
The links below provide you with useful material for this class, including complete lecture notes. These materials will be added by need and more topics will be added.

 Conventional Semantic Approaches


HW2 (due Wednesday, October 3  easy HW, so earlier submission possible and appreciated)

The following exercises related to denotational semantics are from the book material above: Exercises 80, 81, 82 ((page 168; write these up on paper, or in a PDF); Exercise 83 (page 169; do it only in Maude (that is, not on paper) by modifying the provided Maude code for HW2 ).


HW3 (due Monday, October 15)

Combine all the individual extensions of IMP in the provided Maude code for HW3 into the IMP++ language. Read the book material above for all the technical details. You should create a subfolder of imp called 6imp++, and that should have four subfolders, one for each semantic style. Provide also three IMP++ programs.


HW4 (due Monday, October 29)

Same as HW3 but for the three additional semantic approaches discussed in the lecture notes above: MSOS, RSEC, and CHAM. Use this provided Maude code for HW4 . Handle also a short essay discussing the advantages and limitations of each of the semantic approaches discussed so far in class, assigning a (justified) score between 1 and 10 to each of them.

 Category theory: definition, diagrams, cones and limits, exponentials

 Lambda Calculus and Combinatory Logic

 SimplyTyped Lambda Calculus
 Basic notions: type system, equational semantics, models, completeness. Slides
 Cartesian Closed Categories as models for simplytyped lambdacalculus. Slides
HW6 (due Friday, November 30can also take the weekend if needed)

Proposition 8 from the slides on simplytyped lambda calculus. Exercises 5 and 6 from the slides on CCCs.

 Recursion, Types, Polymorphism

ExtraCredit (due Monday, Dec 17)

This can be regarded as "Final exam", but it only counts as extracredit and has the same weight as any of the previous HWs. If you got perfect score so far for the 6 HWs above, then you do not need to do this extracredit. Choose one, and only one, of the following and do it well (you will either get 10 or 0 for this extracredit pb.):
