CS522 - Programming Language Semantics (Spring 2011)

From FSL
Jump to: navigation, search

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: W/F 12:30 - 1:45, 1131 Siebel Center
  • Professor: Grigore Rosu (Office: SC 2110, WWW: http://cs.uiuc.edu/grosu, Email: grosu@cs.uiuc.edu)
  • Office hours: by appointment, very flexible (held by Grigore Rosu in SC 2110)


Web Interface to CS522

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.

  • 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. 25px-Zip_icon.png HERE Info_circle.png 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 (25px-Pdf_icon.png Lecture notes Info_circle.png 25px-Zip_icon.png turing.zip Info_circle.png) (incomplete)
  • Post Correspondence(25px-Pdf_icon.png Lecture notes Info_circle.png 25px-Zip_icon.png post.zip Info_circle.png) (incomplete)
  • Untyped Lambda Calculus and Combinatory Logic 25px-Pdf_icon.png Slides Info_circle.png (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 25px-Zip_icon.png HERE Info_circle.png.
  • Simply Typed Lambda-Calculus
  • Basic notions: type system, equational semantics, models, completeness. 25px-Pdf_icon.png Slides Info_circle.png (incomplete)
  • Category theory: definition, diagrams, cones and limits, exponentials. 25px-Pdf_icon.png Slides Info_circle.png (incomplete)
  • Cartesian Closed Categories as models for simply-typed lambda-calculus. 25px-Pdf_icon.png Slides Info_circle.png (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. 25px-Pdf_icon.png Slides Info_circle.png (incomplete)
  • Polymorphism. 25px-Pdf_icon.png Slides Info_circle.png (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. 25px-Pdf_icon.png Slides Info_circle.png (incomplete)
  • The K Semantic Framework
Personal tools