Difference between revisions of "CS422 - Programming Language Design (Spring 2020)"
Line 61: | Line 61: | ||
Note: See the [https://github.com/kframework/k5/tree/master/k-distribution/tutorial/1_k/3_lambda%2B%2B/lesson_1/exercises/callCC callCC (substitution)], [https://github.com/kframework/k5/tree/master/k-distribution/tutorial/1_k/3_lambda%2B%2B/lesson_1/exercises/from-call-CC-to-callcc from-call-CC-to-callcc (substitution)], [https://github.com/kframework/k5/tree/master/k-distribution/tutorial/1_k/3_lambda%2B%2B/lesson_1/exercises/from-callcc-to-call-CC from-callcc-to-call-CC(substitution)], [https://github.com/kframework/k5/tree/master/k-distribution/tutorial/1_k/3_lambda%2B%2B/lesson_6/exercises/callCC callCC (environment)], [https://github.com/kframework/k5/tree/master/k-distribution/tutorial/1_k/3_lambda%2B%2B/lesson_6/exercises/from-call-CC-to-callcc from-call-CC-to-callcc (environment)], and [https://github.com/kframework/k5/tree/master/k-distribution/tutorial/1_k/3_lambda%2B%2B/lesson_6/exercises/from-callcc-to-call-CC from-callcc-to-call-CC (environment)] exercises in the nightly built for details and test programs. | Note: See the [https://github.com/kframework/k5/tree/master/k-distribution/tutorial/1_k/3_lambda%2B%2B/lesson_1/exercises/callCC callCC (substitution)], [https://github.com/kframework/k5/tree/master/k-distribution/tutorial/1_k/3_lambda%2B%2B/lesson_1/exercises/from-call-CC-to-callcc from-call-CC-to-callcc (substitution)], [https://github.com/kframework/k5/tree/master/k-distribution/tutorial/1_k/3_lambda%2B%2B/lesson_1/exercises/from-callcc-to-call-CC from-callcc-to-call-CC(substitution)], [https://github.com/kframework/k5/tree/master/k-distribution/tutorial/1_k/3_lambda%2B%2B/lesson_6/exercises/callCC callCC (environment)], [https://github.com/kframework/k5/tree/master/k-distribution/tutorial/1_k/3_lambda%2B%2B/lesson_6/exercises/from-call-CC-to-callcc from-call-CC-to-callcc (environment)], and [https://github.com/kframework/k5/tree/master/k-distribution/tutorial/1_k/3_lambda%2B%2B/lesson_6/exercises/from-callcc-to-call-CC from-callcc-to-call-CC (environment)] exercises in the nightly built for details and test programs. | ||
|} | |} | ||
+ | |||
+ | |||
+ | :* '''''SIMPLE: Designing Imperative Programming Languages''''' | ||
+ | ::* [http://www.kframework.org/index.php/K_Tutorial#.5B.3F.3F.27.3F.3F.22.5D_.C2.A0_Part_7:_SIMPLE:_Designing_Imperative_Programming_Languages SIMPLE untyped, statically typed, and dynamically typed] (Part 7 of the K Tutorial) | ||
+ | ::* [http://www.kframework.org/index.php/K_Tutorial#.5B17.2703.22.5D_.C2.A0_Part_5:_Defining_Type_Systems K Tutorial, Part 5: Defining type systems] (this is optional at this stage, but instructive for better understanding the static semantics; read at least Lesson 1, and skim Lesson 6) | ||
+ | ::* {{pdf|CS422-K-Overview.pdf|K Overview}} paper, which also defines and explains SIMPLE. Sections 3 and 4 (the other sections were covered above) |
Revision as of 19:13, 21 February 2020
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-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.
- Meetings: W/F 14:00 - 15:15, 1304 Siebel Center
- Credit: 3 or 4 credits
- Professor: Grigore Rosu (Office: SC 2110)
- Office hours: Held by Grigore Rosu in SC 2110; by appointment.
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
- Introduction
- Structural Operational Semantics
slides
- Book lecture notes on the IMP language, big-step SOS, and small-step SOS (you can skip the rewriting logic and Maude parts; comments welcome!):
IMP-BigStep-SmallStep
- Book lecture notes on the IMP language, big-step SOS, and small-step SOS (you can skip the rewriting logic and Maude parts; comments welcome!):
- Structural Operational Semantics
- K Framework (Official website: http://kframework.org)
- K Tutorial, Part 1: Defining LAMBDA (see the provided video and textual documentation)
- K Tutorial, Part 2: Defining IMP (see the provided video and textual documentation)
- K Tutorial, Part 3: Defining LAMBDA++ (see the provided video and textual documentation)
- K Tutorial, Part 4: Defining IMP++ (see the provided video and textual documentation)
-
K Overview
paper to learn more about K. Sections 1 and 2 (the other sections are optional now; they are covered below)
HW2 (due Wednesday, February 26) ![]() |
---|
Exercise 1 (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 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: See the mu-derived exercise in the nightly built for details and test programs. Exercise 2 (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. Note: See the uninitialized-variables exercise in the nightly built for details and test programs. Exercise 3 (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). Note: See the purely-syntactic exercise in the nightly built for details and test programs. Exercise 4 (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. Note: See the callCC (substitution), from-call-CC-to-callcc (substitution), from-callcc-to-call-CC(substitution), callCC (environment), from-call-CC-to-callcc (environment), and from-callcc-to-call-CC (environment) exercises in the nightly built for details and test programs. |
- SIMPLE: Designing Imperative Programming Languages
- SIMPLE untyped, statically typed, and dynamically typed (Part 7 of the K Tutorial)
- K Tutorial, Part 5: Defining type systems (this is optional at this stage, but instructive for better understanding the static semantics; read at least Lesson 1, and skim Lesson 6)
-
K Overview
paper, which also defines and explains SIMPLE. Sections 3 and 4 (the other sections were covered above)