Students enrolled in this class are expected to check this web page regularly. Complete lecture notes will be posted here.
Course Description
CS422 is an advanced course on principles of programming language design. Major semantic approaches to programming languages will be discussed, such as structural operational semantics (various kinds), denotational semantics, and rewriting logic semantics. Programming language paradigms will be investigated and rigorously defined, including: imperative, functional, object-oriented, and logic programming languages; parameter binding and evaluation strategies; type checking and type inference; concurrency. Since the definitional framework used in this class will be executable, interpreters for the designed languages will be obtained for free. Software analysis tools reasoning about programs in these languages will also arise naturally. Major theoretical models will be discussed.
- Meetings: W/F 12:30 - 13:45, 1131 Siebel Center
- Credit: 3 or 4 credits
- Professor: Grigore Rosu (Office: SC 2110)
- Office hours: 10:00 - 12:00 on Tuesdays (held by Grigore Rosu in SC 2110); also by appointment any other time
Newsgroup
Web Interface to CS422
More info on newgroups at UIUC: https://news.cs.illinois.edu/
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.
- Introduction
slides 
[Lecture 1]
-
-
HW1 (due Wednesday, September 14) 
|
| The following three exercises from the Maude slides: (1) Ex 4, pg 25; (2) Ex 7, pg 39; (3) Ex 8, pg 40.
|
-
- References cited in the book sections below PL-book-references.pdf
-
-
-
| HW2 (due Friday, September 30 - ask for a weekend extension if you really need it)
|
Give formal semanitcs to IMP++ in all styles above. Each individual feature has already been added in the provided imp.zip archive above. Your job is to combine all of these features together into one language.  HW2.zip shows the expected format of your HW2. It also includes a series of IMP++ programs that you may use to test your semantics. Everything you do should go under 6-imp++. You should first complete the imp++-syntax.maude file and make sure you can parse all the programs in imp++-programs.maude. Then add directories for each of the semantics. I created the one for small-step SOS for you and also added a file containing my Maude output when I execute all the provided programs.
|
-
| HW3 (due Friday, October 21 - ask for a weekend extension if you really need it)
|
| Same as HW2, but for MSOS, evaluation contexts and the CHAM. The imp.zip file above may contain several semantics of a certain fetures using the same approach. You can pick any one of them. If you do more, let me know and I may give you extra-credit.
|
-
- K tool - use the K virtual machine (KVM) if you don't want to install it.
| HW4 (due Monday, October 31)
|
Modify IMP++ so that spawn evaluates to a fresh thread identifier (an integer is OK), the identifier of the newly created thread. Moreover, add a join statement construct which takes a thread identifier and blocks until that thread terminates; when that happens, the joining thread continues its execution and the terminated thread dissolves. All these should be done by modifying the imppp.k (currently under examples/languages/research/imppp) definition in the K tool installation above. You should handle three items: (1) the new imppp.k file; (2) the generated imppp.pdf file; and (3) five different programs that use spawn and join. Please use the following syntax:
syntax AExp ::= "spawn" Stmt
syntax Stmt ::= "join" "(" AExp ")"
Although the IMP++ extension in this HW is non-trivial in other semantic frameworks, as you will notice it is acually quite straighforward to do in K once you master the tool. The main purpose of this homework is therefore to install and get familiar with the K tool, which will be very useful for the remaining homeworks.
|
- Defining SIMPLE: An Imperative Language
-
-
-
-
-
| HW5 (due Friday, November 11)
|
This HW has three parts: (1) Add break/continue to while loops in untyped SIMPLE; (2) Add a barrier synchronization statement also to untyped SIMPLE; (3) add typed exceptions to (both statically and dynamically) typed SIMPLE. Use the following syntax:
syntax Stmt ::= "break;" | "continue;" | "barrier;" | "try" Stmt "catch" "(" #Id ":" Type ")" Stmt
The semantics of the barrier is that all threads stop and wait there; once all threads reach the barrier, they all unblock and continue their execution.
|
- Defining KOOL: An Object-Oriented Language
-
-
-
-
-
| HW6 (due Monday, November 28)
|
| Add private methods and fields to KOOL, using the syntax 'private var x ...' and 'private method m ...'. If in doubt, use the semantics of private fields/methods from Java. You have to do these in all three definitions of KOOL: untyped, dynamically typed and statically typed.
|
- Defining FUN: A Functional Language
- Elements of Functional Programming ( slides )
- Type Inference ( slides )
- Untyped FUN
-
| HW7
|
| Define a type inferencer for FUN. Start with the one discussed in class for EXP (found HERE) and keep adding features of FUN to it. As discussed in class, this is an open-ended problem, because you can always make your type inferencer better. Do not atempt to do better than we did in EXP. Do not get stuck with syntax: feel free to change the syntax of FUN to make it more easily parsable, but put a comments in your code explaining what you've done and why. Handle also 5 FUN programs showing that your type inferencer works.
|
