CS522 - Programming Language Semantics (Spring 2012)

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.

HW1 (due Wednesday, Feb 8) Downarrow.png
Add two-variable parallel assignment to IMP in all the discussed semantic approaches. Use the syntax x1,x2 := e1,e2, where x1 and x2 are program variables and where e1 and e2 are expressions. Do it both on paper, using the notation discussed in class, and in Maude.
  • Basic Models of Computation
HW2 (due Friday, Feb 17) Downarrow.png
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 subtracts 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 "...HW2..." 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
HW3 (due Friday, March 2) Downarrow.png
Proposition 4, Exercise 6, Exercise 7, Exercise 9, and Proposition 8.
  • Category theory: definition, diagrams, cones and limits, exponentials. 25px-Pdf_icon.png Slides Info_circle.png
  • Cartesian Closed Categories as models for simply-typed lambda-calculus. 25px-Pdf_icon.png Slides Info_circle.png
HW4 (due Tuesday, March 13) Downarrow.png
Exercises 5 and 6 on CCCs
  • Recursion, Types, Polymorphism
HW5 (due Tuesday, March 27) Downarrow.png
Give PCF a small-step SOS (aka transitional semantics), a big-step SOS (aka as natural semantics), and a denotational semantics. 25px-Zip_icon.png HERE Info_circle.png you can find the sample definitions using these approaches, as well as a generic substitution (in builtins.maude)
HW6 (due Tuesday, April 17) Downarrow.png
Define the type systems of parametric (system F) and of subtype (record-based) polymorphic lambda calculi in Maude, following the same style as for IMP and PCF (see HW5; use the generic substitution provided for HW5). Use the example programs in the lecture notes as tests for your type systems (and handle them as part of HW6, too).
  • Axiomatic Semantics
Personal tools