CS522 - Programming Language Semantics (Spring 2013)

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.illinois.edu/grosu, Email: grosu@illinois.edu)
  • Office hours: Tu 1-3, but also by appointment, very flexible (held by Grigore Rosu in SC 2110)

Newsgroup and Piazza Page

Web Interface to CS522

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.

HW1 (due Tuesday, February 5) Downarrow.png
Do the following exercises, all from the book material above (pages 80/81): Exercise 30; Exercise 32; Exercise 33; Exercise 35 (do it only for the addition); Exercise 36.
  • Conventional Semantic Approaches
HW2 (due Friday, February 15) Downarrow.png
The following exercises are from the book material above. Do them only in Maude (that is, not on paper) by modifying the provided Maude code, with the exception of Exercise 81 which needs to be done only on paper (that is, not in Maude): Exercise 42 (page 92); Exercise 56 (page 137); Exercise 70 (page 155); Exercise 81 (page 168; write this up on paper, or put it into a PDF); Exercise 83 (page 169).
HW3 (due Wednesday, February 27) Downarrow.png
Combine all the individual extensions of IMP provided in the zip archive into the IMP++ language. Read the book material above for all the technical details. You should create a subfolder of imp called 6-imp++, and that should have four subfolders, one for each semantic style. Provide also three IMP++ programs.
HW4 (due Monday, March 11) Downarrow.png
Same as HW3 but for the three additional semantic approaches discussed in the lecture notes above: MSOS, RSEC, and CHAM. 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. For the essay, please use an editor if your handwriting is as bad as mine or worse :)
  • Lambda Calculus and Combinatory Logic
HW5 (due Wednesday, March 27) Downarrow.png
Complete the code snipped above. That covers knowledge about untyped lambda-calculus, fixed-points, combinatory logic, and de Bruijn nameless represenations.
  • Simply-Typed Lambda Calculus
  • Basic notions: type system, equational semantics, models, completeness. 25px-Pdf_icon.png Slides Info_circle.png
HW6 (due Friday, April 5) 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
HW7 (due Friday, April 19---can also take the weekend if needed) Downarrow.png
Exercises 5 and 6 from the slides on CCCs (nothing from the slides on category theory).
  • Recursion, Types, Polymorphism
HW8 (due Tuesday, April 30) Downarrow.png
Consider the PCF language with call-by-value (note that the slides above define the call-by-name variant, but we discussed the changes needed for call-by-value in class). Give it a small-step, a big-step, and a denotational semantics in Maude, using the representations of these semantic approaches discussed in the first part of the class. Provide also 5 (five) PCF programs that can be used to test all three of your semantics. You can use the builtins provided as part of the previous HW (you should only need the generic substitution from there).
Extra credit (due Wednesday, May 8) Downarrow.png
This extracredit HW has the same weight as the previous 8 HWs and is meant to help you increase your overall score, if you want to. It has two problems. The first is to define a type checker for the parametric polymorphic lambda-calculus (or System F). The second is to define a type checker for the subtype polymorphic lambda-calculus. In both cases, make sure that you also include the conditional and a few examples showing that your definition works. Feel free to pick whatever syntax you want for the various constructs (both for terms and for types).
Personal tools