CS422 - Programming Language Design (Fall 2012)

From FSL
Jump to: navigation, search

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: 13:00 - 15:00 on Tuesdays (held by Grigore Rosu in SC 2110); also by appointment any other time (preferred).


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.

  • Conventional Executable Semantics 25px-Pdf_icon.png slides Info_circle.png

HW1 (due Wednesday, September 19) Downarrow.png

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): Combine the two above: add both division-by-zero halting and an increment construct. Feel free to comment on what's going on, particularly on how inconvenient it is to do certain things in SOS (one fo the points of this HW is to understand the limitations of SOS, so you will appreciate K).

Exercise 4 (10 points): The current K LAMBDA semantics of mu (in Lesson 8) is based on substitution, and then letrec is defined as a derived operation using mu. Give mu a different semantics, as a derived construct by translation into other LAMBDA constructs, like we defined with letrec in Lesson 7. To test it, use the same definition of letrec in terms of mu (from Lesson 8) and write 3 recursive programs, like the provided factorial-letrec.lambda.

Note: Always download the latest build of the K tool before any HW or project!!! The latest stable release may be too old.

HW2 (due Friday, October 5) Downarrow.png

Exercise 1 (10 points): Modify the K definition of IMP to not automatically initialize variables to 0. Instead, declared variables should stay uninitialized until assigned a value, and the execution should get stuck when an uninitialized variable is looked up.

Exercise 2 (10 points): Mofify IMP so that the K "followed by" arrow, ~>, does not explicitly occur in the definition (it currently occurs in the semantics of sequential composition). Hint: make sequential composition strict(1) or seqstrict, and have statements reduce to "{}" instead of ".", ... and don't forget to make "{}" a KResult (you may need a new syntactic category for that, which only includes "{}" and is included in KResult).

Exercise 3 (10 points): Define a variant of callcc, say callCC, which never returns to the current continuation unless a value is specifically passed to that continuation. Can you define them in terms of each other? Do these in both the substitution and the environment-based definitions.

Exercise 4 (10 points): The current "halt;" statement of IMP++ only halts the current thread. Define an "abort;" statement which halts the entire program. Write an IMP++ program which shows different behaviors when you replace one of its "halt;" statements with "abort;".

HW3 (due Wednesday, October 17) Downarrow.png

Exercise 1 (10 points): Compilers typically collect all the variables declared in a block and move them all in one place, renaming them appropriately everywhere to avoid name conflicts. Consequently, they do not like you to declare a variable twice in the same block. Modify the K type system of IMP++ to reject programs which declare the same variable twice in a block. Your resulting type system should get stuck when a variable is declared the second time.

Exercise 2 (10 points): Mofify the substitution-based type system of LAMBDA to type the let and letrec constructs directly, without desugating them to lambda, application and/or mu.

Exercise 3 (10 points): Same as Exercise 2, but for the environment-based type system of LAMBDA

  • SIMPLE: Designing Imperative Programming Languages
HW4 (due Wednesday, October 31) Downarrow.png

Exercise 1 (10 points): Add "break;" and "continue;" to untyped SIMPLE. Just take the semantics of these from C/C++/Java, if uncertain. Do only the simple, unlabeled ones, which only break the innermost loop. One thing to think about: do you still want to desugar the for-loop into a while-loop as we do it now?

Exercise 2 (10 points): Our current exceptions in SIMPLE are quite simplistic: the thrown exceptional value is caught by the innermost try-catch statement, and you get a runtime error (stuck) if the type of the thrown value is not the same as the type of the exception's parameter. They work fine if you restrict them to only throw and catch integer values, like we did in the static semantics, but modern languages do not like this limitation. Change the existing dynamic semantics of typed SIMPLE to propagate a thrown exception to the outer try-catch statement when the inner one cannot handle the exception due to a type mismatch. For example, "try { try { throw 7; } catch(bool x) {print(1};} } catch{int x) {print(2);}" should print 2, not get stuck as it currently happens.

Exercise 3 (10 points): Same as Pb2, but for the static semantics of the typed SIMPLE.

For the first 2 problems, also provide ONE tricky test program for each, together with a short description of what it should do. You will get an extra-point if your program breaks everybody's definition (except potentially yours).  :-)

  • KOOL: Designing Object-Oriented Programming Languages
HW5 (due Wednesday, November 14) Downarrow.png

Exercise 1 (10 points): Currently, all class members (fields and/or methods) are public in KOOL. Sometimes we want to keep members of a class private, in the sense that subclasses do not have direct access to those members. This exercise asks you to add private members to untyped KOOL. Syntactically, you should allow a new keyword, "private", to optionally prepend member declarations. For example, "private var x=10, y=10;" or "private method f(x,y) {...}". Semantically, the pivate members should have the same semantics as in conventional OO programming languages, say Java. Feel free to pick another language as a model if you want to (e.g., C++, C#, etc.), but make that clear in your submission. Also, feel free to make reasonable simplifying syntactic assumptions about programs if you need or want to (for example, the private members have distinct names, etc.).

Exercise 2 (10 points): Same as Exercise 1, but for dynamically typed KOOL.

Exercise 3 (10 points): Same as Eercises 1 and 2, but for statically typed KOOL.

  • FUN: Designing Functional Programming Languages
  • FUN untyped (also part of the latest K built)
  • Tutorial 5, Lesson 9: Let-Polymorphic Type Inference (read also Lessons 4, 5, 6, 7, 8 for better understanding)
HW6 (due Friday, December 7) Downarrow.png

Exercise (10 points): Define a let-polymorphic type inferencer for FUN. Follow the model in Lesson 9 of Tutorial 5 (see above, and also in the latest K distribution). Call the resulting K definition FUN-TYPE-INFERENCE and put it in a file named fun-type-inference.k. If you also provide new programs (besides those already provided under examples/fun/programs), they will be used during grading (so it is in your interest to provide tricky ones). Do not worry about typing callcc; I will not include tests for it.

Extra-credit HW (due by the end of the semester -- before the Reading day) Downarrow.png

Exercise (5 points added your final course score, on a scale 0-100): Give a substitution-based semantics to FUN. You may want to refresh your memory on substitution- vs. environment-based definitions by redoing the LAMBDA/LAMBDA++ tutorial. You will still need the store cell, to store the values that references point to, but there should be no environment anymore in your new configuration.

  • LOGIK: Designing Logic Programming Languages
  • LOGIK (also part of the latest K built)

  • Sample Finals (from past iterations of CS422, reverse chronological order)
Personal tools