Difference between revisions of "CS522 - Programming Language Semantics (Fall 2018)"

From FSL
Jump to: navigation, search
(Created page with "Students enrolled in this class are expected to check this web page regularly. Lecture notes and important other material will be posted here. ==Course Description== CS522 ...")
 
(Lecture Notes, Useful Material)
 
(35 intermediate revisions by one user not shown)
Line 5: Line 5:
 
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.
 
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 9:30 - 10:45, 1103 Siebel Center
+
* ''Meetings'': Tu/Th 9:30 - 10:45, 1103 Siebel Center
 
* ''Professor'': Grigore Rosu (Office: SC 2110, WWW: http://fsl.cs.illinois.edu/grosu, Email: grosu@illinois.edu)
 
* ''Professor'': Grigore Rosu (Office: SC 2110, WWW: http://fsl.cs.illinois.edu/grosu, Email: grosu@illinois.edu)
 
* ''Office hours'': By appointment, very flexible (held by Grigore Rosu in SC 2110)
 
* ''Office hours'': By appointment, very flexible (held by Grigore Rosu in SC 2110)
Line 18: Line 18:
  
 
:* {{pdf|CS522-Fall-2018-Introduction.pdf|'''''Introduction'''''}}
 
:* {{pdf|CS522-Fall-2018-Introduction.pdf|'''''Introduction'''''}}
:* '''''Rewriting Logic and Maude'''''
 
  
 
:* '''''Conventional Semantic Approaches'''''
 
:* '''''Conventional Semantic Approaches'''''
 +
::* {{pdf|CS522-Fall-2018-Conventional-Executable-Semantics.pdf|Slides (PDF)}} {{zip|CS522-Fall-2018-Conventional-Executable-Semantics.pptx|Slides (PPTX)}} <font color=red>(incomplete)</font>
 +
::* {{pdf|CS522-Fall-2018-basic-semantics.pdf|Book material on IMP, Big-Step SOS, Small-Step SOS, and Denotational Semantics}}
 +
::* '''''Rewriting Logic and Maude'''''
 +
:::* {{pdf|CS522-Fall-2018-Maude.pdf|slides}} - recommended only for a quick look
 +
:::* {{pdf|CS522-Fall-2018-Maude-book.pdf|Book material}} - recommended
 +
{| border="1" cellpadding="5" cellspacing="0" width="100%"
 +
! style="background:#ccddcc;" align="left" | '''''<font color=red>HW1 (due Tuesday, September 18)</font>''''' [[Image:downarrow.png]]
 +
|-
 +
| The following exercises are from the book material above.  Do them only in Maude (that is, ''not'' on paper) by modifying {{zip|CS522-Fall-2018-Maude-HW1.zip|the provided Maude code for HW1}}): Exercise 56 (page 137); Exercise 70 (page 155).
 +
In case you are not familiar with Maude, you are encouraged to do the following exercises to warm-up (but please do not include them as part of your HW1 submission): Exercise 30; Exercise 32; Exercise 33; Exercise 35; Exercise 36.  All at pages 80/81.
 +
|}
 +
 +
{| border="1" cellpadding="5" cellspacing="0" width="100%"
 +
! style="background:#ccddcc;" align="left" | '''''<font color=red>HW2 (due Wednesday, October 3 - easy HW, so earlier submission possible and appreciated)</font>''''' [[Image:downarrow.png]]
 +
|-
 +
| The following exercises related to denotational semantics are from the book material above: Exercises 80, 81, 82 ((page 168; write these up on paper, or in a PDF); Exercise 83 (page 169; do it only in Maude (that is, ''not'' on paper) by modifying {{zip|CS522-Fall-2018-Maude-HW2.zip|the provided Maude code for HW2}}).
 +
|}
 +
::* {{pdf|CS522-Fall-2018-IMP++.pdf|Book material on IMP++: Challenging Big-Step SOS, Small-Step SOS, and Denotational Semantics}}
 +
{| border="1" cellpadding="5" cellspacing="0" width="100%"
 +
! style="background:#ccddcc;" align="left" | '''''<font color=red>HW3 (due Monday, October 15)</font>''''' [[Image:downarrow.png]]
 +
|-
 +
| Combine all the individual extensions of IMP in {{zip|CS522-Fall-2018-Maude-HW2.zip|the provided Maude code for HW3}} into the IMP++ language.  Read the book material above for all the technical details.  You should create a subfolder of imp called 6-imp++, and that should have four subfolders, one for each semantic style.  Provide also three IMP++ programs.
 +
|}
 +
::* {{pdf|CS522-Fall-2018-MSOS-RSEC-CHAM.pdf|Book material on Modular SOS, Evaluation Contexts, and the CHAM}}
 +
{| border="1" cellpadding="5" cellspacing="0" width="100%"
 +
! style="background:#ccddcc;" align="left" | '''''<font color=red>HW4 (due Monday, October 29)</font>''''' [[Image:downarrow.png]]
 +
|-
 +
| Same as HW3 but for the three additional semantic approaches discussed in the lecture notes above: MSOS, RSEC, and CHAM.  Use {{zip|CS522-Fall-2018-Maude-HW4.zip|this provided Maude code for HW4}}.  Handle also a short essay discussing the advantages and limitations of each of the semantic approaches discussed so far in class, assigning a (justified) score between 1 and 10 to each of them.
 +
|}
 +
 +
:* '''''Category theory: definition, diagrams, cones and limits, exponentials'''''
 +
::* {{pdf|CS522-Fall-2018-Category-Theory-slides.pdf|Slides}}
 +
::* {{zip|CS522-Fall-2018-HandWritten-Category-Theory.zip|Hand written notes on category theory properties}}
  
 
:* '''''Lambda Calculus and Combinatory Logic'''''
 
:* '''''Lambda Calculus and Combinatory Logic'''''
 +
::* {{pdf|CS522-Fall-2018-Lambda-slides.pdf|Slides}}
 +
::* {{pdf|CS522-Fall-2018-Lambda.pdf|Book material on Lambda Calculus and Combinatory Logic}}
 +
::* {{zip|CS522-Fall-2018-HandWritten-CCC-untyped-lambda.zip|Hand written notes on CCC models of untyped Lambda Calculus}}
 +
{| border="1" cellpadding="5" cellspacing="0" width="100%"
 +
! style="background:#ccddcc;" align="left" | '''''<font color=red>HW5 (due Monday, November 12)</font>''''' [[Image:downarrow.png]]
 +
|-
 +
| This is a theoretical HW, requiring you to do three proofs using category theory.  You are strongly encouraged to do *all* the exercises in the slides, especially if you did not have prior experience with category theory.  However, for his HW, only handle the following three exercises: (1, easy) Exercise 8 on slide 20 in the {{pdf|CS522-Fall-2018-Category-Theory-slides.pdf|category theory slides}}; (2, easy) Property 1 on `category theory - 3.png` in the {{zip|CS522-Fall-2018-HandWritten-Category-Theory.zip|hand written notes on category theory properties}}; and (3, harder) Lemma on slide `ccc-untyped-lambda - 3.png` in the {{zip|CS522-Fall-2018-HandWritten-CCC-untyped-lambda.zip|hand written notes on CCC models of untyped lambda calculus}}.
 +
|}
  
 
:* '''''Simply-Typed Lambda Calculus'''''
 
:* '''''Simply-Typed Lambda Calculus'''''
::* Category theory: definition, diagrams, cones and limits, exponentials.
+
::* Basic notions: type system, equational semantics, models, completeness. {{pdf|CS522-Fall-2018-Simply-Typed-Lambda-Calculus.pdf|Slides}}
::* Cartesian Closed Categories as models for simply-typed lambda-calculus.
+
::* Cartesian Closed Categories as models for simply-typed lambda-calculus. {{pdf|CS522-Fall-2018-PL-CCC.pdf|Slides}}
 +
{| border="1" cellpadding="5" cellspacing="0" width="100%"
 +
! style="background:#ccddcc;" align="left" | '''''<font color=red>HW6 (due Friday, November 30---can also take the weekend if needed)</font>''''' [[Image:downarrow.png]]
 +
|-
 +
| Proposition 8 from the slides on simply-typed lambda calculus.  Exercises 5 and 6 from the slides on CCCs.
 +
|}
  
 
:* '''''Recursion, Types, Polymorphism'''''
 
:* '''''Recursion, Types, Polymorphism'''''
::* Recursion and Types.
+
::* Recursion and Types. {{pdf|CS522-Fall-2018-Recursion.pdf|Slides}}
::* Polymorphism.
+
::* Polymorphism. {{pdf|CS522-Fall-2018-Polymorphism.pdf|Slides}}
 +
{| border="1" cellpadding="5" cellspacing="0" width="100%"
 +
! style="background:#ccddcc;" align="left" | '''''<font color=red>Extra-Credit (due Monday, Dec 17) </font>''''' [[Image:downarrow.png]]
 +
|-
 +
| This can be regarded as "Final exam", but it only counts as HW (and not project) extra-credit and has the same weight as any of the previous HWs.  If you got perfect score so far for the 6 HWs above, then you do not need to do this extra-credit.  Choose one, and only one, of the following and do it well (you will get either 10 or 0 for this extra-credit problem!):
 +
<br> (1) Complete this {{zip|CS522-Fall-2018-Lambda-Extra.zip|LAMBDA code snippet}}.  This covers knowledge about untyped lambda-calculus, fixed-points, combinatory logic, and de Bruijn nameless representations.
 +
<br> (2) Consider the PCF language with call-by-value (note that the slides above define the call-by-name variant).  Give it a small-step, a big-step, and a denotational semantics in Maude, using the representations of these semantic approaches discussed in the first part of the class.  Provide also 5 (five) PCF programs that can be used to test all three of your semantics.  You can use the builtins provided as part of the previous HWs (you should only need the generic substitution from there).
 +
<br> (3) This has two problems.  The first is to define a type checker for the parametric polymorphic lambda-calculus (or System F).  The second is to define a type checker for the subtype polymorphic lambda-calculus.  In both cases, make sure that you also include the conditional and a few examples showing that your definition works.  Feel free to pick whatever syntax you want for the various constructs (both for terms and for types).
 +
|}

Latest revision as of 14:40, 6 December 2018

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: Tu/Th 9:30 - 10:45, 1103 Siebel Center
  • Professor: Grigore Rosu (Office: SC 2110, WWW: http://fsl.cs.illinois.edu/grosu, Email: grosu@illinois.edu)
  • Office hours: By appointment, very flexible (held by Grigore Rosu in SC 2110)

[edit] Piazza Page

CS522 Piazza Page

[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 and more topics will be added.

  • Conventional Semantic Approaches
HW1 (due Tuesday, September 18) Downarrow.png
The following exercises are from the book material above. Do them only in Maude (that is, not on paper) by modifying 25px-Zip_icon.png the provided Maude code for HW1 Info_circle.png): Exercise 56 (page 137); Exercise 70 (page 155).

In case you are not familiar with Maude, you are encouraged to do the following exercises to warm-up (but please do not include them as part of your HW1 submission): Exercise 30; Exercise 32; Exercise 33; Exercise 35; Exercise 36. All at pages 80/81.

HW2 (due Wednesday, October 3 - easy HW, so earlier submission possible and appreciated) Downarrow.png
The following exercises related to denotational semantics are from the book material above: Exercises 80, 81, 82 ((page 168; write these up on paper, or in a PDF); Exercise 83 (page 169; do it only in Maude (that is, not on paper) by modifying 25px-Zip_icon.png the provided Maude code for HW2 Info_circle.png).
HW3 (due Monday, October 15) Downarrow.png
Combine all the individual extensions of IMP in 25px-Zip_icon.png the provided Maude code for HW3 Info_circle.png into the IMP++ language. Read the book material above for all the technical details. You should create a subfolder of imp called 6-imp++, and that should have four subfolders, one for each semantic style. Provide also three IMP++ programs.
HW4 (due Monday, October 29) Downarrow.png
Same as HW3 but for the three additional semantic approaches discussed in the lecture notes above: MSOS, RSEC, and CHAM. Use 25px-Zip_icon.png this provided Maude code for HW4 Info_circle.png. Handle also a short essay discussing the advantages and limitations of each of the semantic approaches discussed so far in class, assigning a (justified) score between 1 and 10 to each of them.
  • Category theory: definition, diagrams, cones and limits, exponentials
  • Lambda Calculus and Combinatory Logic
HW5 (due Monday, November 12) Downarrow.png
This is a theoretical HW, requiring you to do three proofs using category theory. You are strongly encouraged to do *all* the exercises in the slides, especially if you did not have prior experience with category theory. However, for his HW, only handle the following three exercises: (1, easy) Exercise 8 on slide 20 in the 25px-Pdf_icon.png category theory slides Info_circle.png; (2, easy) Property 1 on `category theory - 3.png` in the 25px-Zip_icon.png hand written notes on category theory properties Info_circle.png; and (3, harder) Lemma on slide `ccc-untyped-lambda - 3.png` in the 25px-Zip_icon.png hand written notes on CCC models of untyped lambda calculus Info_circle.png.
  • Simply-Typed Lambda Calculus
  • Basic notions: type system, equational semantics, models, completeness. 25px-Pdf_icon.png Slides Info_circle.png
  • Cartesian Closed Categories as models for simply-typed lambda-calculus. 25px-Pdf_icon.png Slides Info_circle.png
HW6 (due Friday, November 30---can also take the weekend if needed) Downarrow.png
Proposition 8 from the slides on simply-typed lambda calculus. Exercises 5 and 6 from the slides on CCCs.
  • Recursion, Types, Polymorphism
Extra-Credit (due Monday, Dec 17) Downarrow.png
This can be regarded as "Final exam", but it only counts as HW (and not project) extra-credit and has the same weight as any of the previous HWs. If you got perfect score so far for the 6 HWs above, then you do not need to do this extra-credit. Choose one, and only one, of the following and do it well (you will get either 10 or 0 for this extra-credit problem!):


(1) Complete this 25px-Zip_icon.png LAMBDA code snippet Info_circle.png. This covers knowledge about untyped lambda-calculus, fixed-points, combinatory logic, and de Bruijn nameless representations.
(2) Consider the PCF language with call-by-value (note that the slides above define the call-by-name variant). Give it a small-step, a big-step, and a denotational semantics in Maude, using the representations of these semantic approaches discussed in the first part of the class. Provide also 5 (five) PCF programs that can be used to test all three of your semantics. You can use the builtins provided as part of the previous HWs (you should only need the generic substitution from there).
(3) This has two problems. The first is to define a type checker for the parametric polymorphic lambda-calculus (or System F). The second is to define a type checker for the subtype polymorphic lambda-calculus. In both cases, make sure that you also include the conditional and a few examples showing that your definition works. Feel free to pick whatever syntax you want for the various constructs (both for terms and for types).

Personal tools
Namespaces

Variants
Actions
Navigation