CS522 - Programming Language Semantics (Spring 2011)
Students enrolled in this class are expected to check this web page regularly. Lecture notes and important other material will be posted here.
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: W/F 12:30 - 1:45, 1131 Siebel Center
- Professor: Grigore Rosu (Office: SC 2110, WWW: http://cs.uiuc.edu/grosu, Email: firstname.lastname@example.org)
- Office hours: by appointment, very flexible (held by Grigore Rosu in SC 2110)
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.
- Conventional Executable Semantics
- Homeworks 1 & 2 (due Feb 25, midnight): Define the IMP++ language in all semantic approaches. IMP++ is the extension of IMP with ALL five language features discussed and defined in class (increment, output, halting, threads, and local variables). Each semantics must be executable when run using Maude. HERE you can find the Maude definition of each of IMP's extension in each of the semantic approaches. You are suppossed to add a new top-level directory, 6-imp++, which should contain 7 (seven) subdirectories, one for each semantics. For the CHAM, it suffices to pick one of the state-based or the environment-store-based approaches.
- Basic Models of Computation
- Turing Machines ( Lecture notes turing.zip ) (incomplete)
- Post Correspondence( Lecture notes post.zip ) (incomplete)
- Untyped Lambda Calculus and Combinatory Logic Slides (incomplete)
- Homework 3 (due March 15, midnight): Define the following in Maude: untyped substitution-based lambda-calculus, de Bruijn lambda-calculus and combinatory logic, as well translations from the former to the latter two; a Turing machine which multiplies two natural numbers; a way to use the Post correspondence problem to compute the least common multiply of two positive natural numbers. Do all these by replacing "...HW3..." with appropriate Maude code HERE .
- Simply Typed Lambda-Calculus
- Basic notions: type system, equational semantics, models, completeness. Slides (incomplete)
- Category theory: definition, diagrams, cones and limits, exponentials. Slides (incomplete)
- Cartesian Closed Categories as models for simply-typed lambda-calculus. Slides (incomplete)
- Homework 4 (due March 25, midnight): Proposition 4, Exercise 6, Exercise 9, Proposition 8 from simply-typed lambda-calculus; Exercises 3, 7 and 8 from category theory; and Exercises 5 and 6 from CCCs.
- Recursion, Types, Polymorphism
- Recursion and Types. Slides (incomplete)
- Polymorphism. Slides (incomplete)
- Homework 5 (due April 17, midnight): (1) Define call-by-value PCF using any of the semantic approaches discussed in the first part of the course; you get extracredit if you define it in more than one approach. (2) Define the parametric polymorphic type checker of System F (see also Exercise 2 on page 8). (3) Define the syntax-directed subtype polymorphic type checker of the discussed simply-typed lambda calculus extended with records (see also Exercise 21 on page 63). Define each of the above using Maude. The former will result in an interpreter for PCF, while the latter two in type checkers for the corresponding calculi. For each definition, also add at least 5 examples (it is in your interest to have as many and hard examples as possible, because I'm going to grade HW5 using as test suite the union of your examples).
- Axiomatic Semantics
- Hoare Logic. Slides (incomplete)
- The K Semantic Framework