Difference between revisions of "CS522 - Programming Language Semantics (Spring 2012)"
From FSL
Line 71: | Line 71: | ||
::* Polymorphism. {{pdf|CS522-Spring-2012-PL-Polymorphism.pdf|Slides}} | ::* Polymorphism. {{pdf|CS522-Spring-2012-PL-Polymorphism.pdf|Slides}} | ||
+ | |||
+ | {| border="1" cellpadding="5" cellspacing="0" width="100%" | ||
+ | ! style="background:#ccddcc;" align="left" | '''''<font color=red>HW6 (due Tuesday, April 17)</font>''''' [[Image:downarrow.png]] | ||
+ | |- | ||
+ | | Define the type systems of parametric (system F) and of subtype (record-based) polymorphic lambda calculi in Maude, following the same style as for IMP and PCF (see HW5; use the generic substitution provided for HW5). Use the example programs in the lecture notes as tests for your type systems (and handle them as part of HW6, too). | ||
+ | |} | ||
:* '''''Axiomatic Semantics''''' | :* '''''Axiomatic Semantics''''' | ||
::* Hoare Logic. {{pdf|CS522-Spring-2012-PL-Hoare.pdf|Slides}} | ::* Hoare Logic. {{pdf|CS522-Spring-2012-PL-Hoare.pdf|Slides}} |
Latest revision as of 17:15, 11 April 2012
Students enrolled in this class are expected to check this web page regularly. Lecture notes and important other material will be posted here.
[edit] Course Description
CS522 is an advanced course on semantics of programming languages. Various semantic approaches and related aspects will be defined and investigated. Executable semantics of various programming languages and paradigms will be discussed, together with major theoretical models.
- Meetings: W/F 12:30 - 1:45, 1131 Siebel Center
- Professor: Grigore Rosu (Office: SC 2110, WWW: http://cs.uiuc.edu/grosu, Email: grosu@cs.uiuc.edu)
- Office hours: by appointment, very flexible (held by Grigore Rosu in SC 2110)
[edit] Newsgroup
[edit] 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
- Conventional Semantic Approaches
- Basic Models of Computation
- Turing Machines ( Lecture notes turing.zip ) (incomplete)
- Post Correspondence( Lecture notes post.zip ) (incomplete)
- Untyped Lambda Calculus and Combinatory Logic Slides (incomplete)
HW2 (due Friday, Feb 17) |
---|
Define the following in Maude: untyped substitution-based lambda-calculus, de Bruijn lambda-calculus and combinatory logic, as well translations from the former to the latter two; a Turing machine which subtracts two natural numbers; a way to use the Post correspondence problem to compute the least common multiply of two positive natural numbers. Do all these by replacing "...HW2..." with appropriate Maude code HERE . |
- Simply Typed Lambda-Calculus
- Basic notions: type system, equational semantics, models, completeness. Slides
HW3 (due Friday, March 2) |
---|
Proposition 4, Exercise 6, Exercise 7, Exercise 9, and Proposition 8. |
- Category theory: definition, diagrams, cones and limits, exponentials. Slides
- Cartesian Closed Categories as models for simply-typed lambda-calculus. Slides
HW4 (due Tuesday, March 13) |
---|
Exercises 5 and 6 on CCCs |
- Recursion, Types, Polymorphism
- Recursion and Types. Slides
HW5 (due Tuesday, March 27) |
---|
Give PCF a small-step SOS (aka transitional semantics), a big-step SOS (aka as natural semantics), and a denotational semantics. HERE you can find the sample definitions using these approaches, as well as a generic substitution (in builtins.maude) |
- Polymorphism. Slides
- Axiomatic Semantics
- Hoare Logic. Slides