Formal Systems Laboratory

CS422 - Programming Language Design (Fall 2024)

Students enrolled in this class are expected to check this web page regularly. Complete lecture notes will be posted here, following the same model as in CS422 in Fall 2023.

We may sometimes meet online on zoom, eg when traveling to professional events: https://illinois.zoom.us/j/2172447431?pwd=dEtxWmdJR0FYOElUa1ZLL2RJRzdZUT09

Lecture Recordings

When we meet online, we will record the lectures and post the links here:

Sept 3

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-based 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.

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 date: Tuesday, Sept 17th, AoE)

Exercise 1 (10 points): Modify IMP (its Big-Step and its Small-Step SOS) to halt when a division-by-zero takes place, returning a configuration holding the state in which the division by zero took place.

Exercise 2 (10 points): Add a variable increment construct, ++x (increment x and return the incremented value), to IMP: first add it to the formal BNF syntax, then to the Big-Step SOS, then to the type-system, and then to the Small-Step SOS.

Exercise 3 (10 points): Add I/O constructs, read() and print(AExp) to IMP: first add these to the formal BNF syntax (read() is an AExp construct and print(AExp) is a Stmt construct), then to the Big-Step SOS, then to the type-system, and then to the Small-Step SOS.

Exercise 4 (10 points): Combine the three above: add division-by-zero halting, an increment construct, and the two I/O constructs to IMP. Feel free to comment on what’s going on, particularly on how inconvenient it is to do certain things in SOS (one of the points of this HW is to understand the limitations of SOS, so you will appreciate K).

HW2 (due date: Tuesday, Oct 8th, AoE)

Do the exercises in the K Tutorial. They are spread through the lessons in Section 1, as well as in Section 2.1 (the other lessons are not finished yet). Create a github repo, possibly as a clone of the K tutorial, and add the exercises there in the appropriate folders using any naming convention you prefer. When done, give me access to view your repo and send me an email to confirm that I have access. My github ID is grosu.