CS422 - Programming Language Design (Spring 2010)

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: Tu/Th 3:30 - 4:45, 1302 Siebel Center
Credit: 3 or 4 credits
Professor: Grigore Rosu (Office: SC 2110)
Office hours: 10:00 - 12:00 on Mondays (held by Grigore Rosu in SC 2110)


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.

  • 25px-Pdf_icon.png Introduction Info_circle.png
  • 25px-Pdf_icon.png [F1] Operational Semantics Info_circle.png (use these slides only for principles; the actual IMP language slightly changed; check the subitems below for detailed information and please do not refrain from reporting typos, errors, etc.; also, your feedback is highly appreciated)
  • 25px-Pdf_icon.png [F2] Maude Info_circle.png
  • IMP
  • 25px-Pdf_icon.png [F5] Notes on big-step SOS Info_circle.png [complete]
  • Homework 1, due Tuesday, Feb 9, by midnight (email to grosu@illinois.edu): (1) [F2, Maude] Ex 4, pg 24; (2) [F2, Maude] Ex 9, pg 55; (3) [F5, BigStep] Ex 32, pg 76, only change the Maude code (related to big-step SOS) provided in [F3]; (4) [F5, BigStep] Ex 33, pg 77, only change the Maude code (related to big-step SOS) provided in [F3]
  • 25px-Pdf_icon.png [F6] Notes on small-step SOS Info_circle.png [complete]
  • 25px-Pdf_icon.png [F7] Notes on MSOS Info_circle.png [complete]
  • Homework 2, due Tuesday, Feb 23, by midnight (email to grosu@illinois.edu): [F6, SmallStep] Ex 37 (pg 90), Ex 38 (pg 91), Ex 39 (pg 92), Ex 40 (pg 92), Ex 42 (pg 93); only change the Maude code related to small-step SOS provided in [F3] (see also Figure 3.16 on pg 99 in [F6]). [F7, MSOS] Ex 48, Ex 49, Ex 50, Ex 51 (all on pg 106); only change the Maude code related to MSOS provided in [F3] (see also Figure 3.21 on pg 113 in [F7]). As part of HW2, you should therefore handle 9 Maude files; call them Ex48.maude, etc.
  • 25px-Pdf_icon.png [F8] Notes on Reduction Semantics with Evaluation Contexts Info_circle.png [complete]
  • 25px-Pdf_icon.png [F9] Notes on IMP++ Info_circle.png [incomplete in general, but complete for HW3]
  • Homework 3, due Tuesday, Mar 9, by midnight (email to grosu@illinois.edu): [F8, RSEC] Ex 75, Ex 76; [F9, IMP++] Ex 81, Ex 82, Ex 83, Ex 84, Ex 86, Ex 87, Ex 88, Ex 89, Ex 92, Ex 93, Ex 94, Ex 95. All exercises in this HW should modify the Maude code in [F3]. Skip anything unrelated to Maude in these exercises. In the case of reduction semantics with evaluation contexts, it suffices to only modify its 3rd embedding into rewrite logic. Call the Maude files Ex75.maude, etc.
  • 25px-Pdf_icon.png [F10] Denotational Semantics Info_circle.png (like for operational semantics, use these slides only for concepts and principles)
  • 25px-Pdf_icon.png [F11] The K Framework Info_circle.png [incomplete, last update March 29; however, this is more than sfficient for HW4]
  • Homework 4, due Tuesday, Mar 23, by midnight (email to grosu@illinois.edu); since this falls in the middle of the break, if you want you can handle HW4 by the following Tuesday, March 30 (one more week): Ex 1,2: Same like Ex 75,76 in HW3, but for the denotational semantics of IMP in [F3] instead of RSEC. Ex 3,4: same as Ex 1,2, but for the K semantics in [F3] (you may also want to check [F11]). Ex 5: the exercise on page 29, in [F10] above
  • 25px-Pdf_icon.png The CHALLENGE Language Info_circle.png [incomplete, last update March 15]
  • Formal Semantics of Imperative Programming Languages
  • Homework 5, due Friday, April 16, by midnight (email to grosu@illinois.edu); if you really need it, you can take two more days, until April 18.: Add to the SIMPLE language exceptions (with syntax try Stmt catch(Id) Stmt' and throw(Exp), as discussed in class) and threads with spawn and acquire/release sincronization (like in the CHALLENGE language). You should modify the untyped, the dynamically typed and the statically typed definitions of SIMPLE in K-Maude. You can assume that an exception must be caught by the most nested try/catch block also in the case of the typed SIMPLE; in other words, the type of the identifier that the thrown value is bound to should not determine the behavior of try/catch. Feel free to throw a "-1" implicit exception when a division by 0 takes place (though you don't lose points if you don't do it). HERE you can find information on how to download K-Maude and SIMPLE.
  • Formal Semantics of Functional Programming Languages
  • Homework 6, due Tuesday, May 4, by midnight (email to grosu@illinois.edu); since this is the last hw, if you need it you can take until the Reading day to finish this one.: (1) Define loops with break and continue in FUN using callcc. Feel free to inspire yourself from the definition of try/catch in p27-3 and also to make any assumptions that you need to make your life easier. Give also 3 example programs to convince that your definition works. (2) Define a type inferencer for FUN. This problem is the hardest you had so far and it is open ended, in that you can define the type inferencer as general as you want to. You may use the provided EXP type inferencer as a source of inspiration. The role of this exercise is to expose you to research, so I will be forgiving when I grade it. Do these problems using the latest version of the K tool, downloadable as explained in HW5.
  • Formal Semantics of Object-Oriented Languages


Unit Project

Information on the unit project will be available at the right moment.

Personal tools