CS520 Theory of Programming Languages, Fall 2020, KAIST

This is a webpage of the course "CS520 Theory of Programming Languages", which is offered at the KAIST CS department in the fall of 2020. The webpage will contain links to course-related materials and announcements.

CS520 is an advanced graduate-level course on the theories of programming languages. Its goal is to expose students to rigorous mathematical foundations for programming languages and systems, and mathematical techniques for formally reasoning about programs written in those languages. The course will largely follow Reynolds's textbook "Theories of Programming Languages", which provides good mathematical treatment of a wide range of programming constructs through axiomatic, denotational and operational semantics.

The prerequisite of the course is CS320, the undergraduate-level programming-language course offered at KAIST, or a similar course. The course will be heavy in math, and we expect students to be comfortable with doing and reading rigorous mathematical proofs.

1. Important Announcements

[December 4] No Q&A Session on 9 December.

Based on what I was told, it is very likely that the interviews for the KAIST undergraduate admission will happen offline on Wed and Thu next week. I am aware that some graduate students participate in online classes in their offices, but this face-to-face interview means that all of their offices will be closed. Furthermore, I think that during this undergraduate interview period, it is better to stay away from the university, not only because of the interview but also because of COVID-19. So, we decide to cancel our Q&A session on Wednesday next week; there will not be an online class on Wednesday.

On Monday, we will have a Q&A session as planned, based on the questions that students posted at KLMS Q&A.

[November 22] Q&A Sessions on 7 and 9 December.

On the 7th and 9th of December, we will have Q&A sessions in our online classes instead of me explaining new materials. If you want some questions to be discussed, leave comments about those questions in my KLMS annoucement about these Q&A sessions.

[November 22] Homework4 is out.

The homework assignment 4 is out. This is the last homework assignment. Submit your solutions in KLMS by 6:00pm on 7 December 2020 (Monday).

We remind the students that we adopt a very strict policy for handling dishonest behaviours. If a student is found to copy answers from peers or other sources in her or his submission for this homework assignment, he or she will get F.

[November 15] Homework3 is out.

The homework assignment 3 is out. Submit your solutions in KLMS by 6:00pm on 25 November 2020 (Wednesday).

We remind the students that we adopt a very strict policy for handling dishonest behaviours. If a student is found to copy answers from peers or other sources in her or his submission for this homework assignment, he or she will get F.

[October 11] Homework2 is out.

The homework assignment 2 is out. Submit your solutions in KLMS by 6:00pm on 28 October 2020 (Wednesday).

We remind the students that we adopt a very strict policy for handling dishonest behaviours. If a student is found to copy answers from peers or other sources in her or his submission for this homework assignment, he or she will get F.

[September 20] Policy for handling late submissions.

We will adopt the following scheme for handling late submissions for homework assignments and critical surveys. The scheme assumes that the total marks are 100.

1. <= One day late (by the midnight of the next day): -10
2. <= Two days late: -20
3. <= Three days late: -30
4. <= Four days late: -40
5. More than four days late: -100.

Of course, we won't accept any late submissions for the final exam.

[September 20] Homework1 is out.

The homework assignment 1 is out. Submit your solutions in KLMS by 6:00pm on 5 October 2020 (Monday).

We remind the students that we adopt a very strict policy for handling dishonest behaviours. If a student is found to copy answers from peers or other sources in her or his submission for this homework assignment, he or she will get F.

2. Logistics

Evaluation

• Final exam (40%). Homework (30%). Two critical surveys (30%).

Teaching Staffs

• Lecturer: Prof Hongseok Yang (email: [email protected], office hour: 6:00pm - 7:00pm Monday in ZOOM. You can find more information about it in KLMS.)
• TA: Hyoungjin Lim (email: [email protected])
• TA: Dongwoo Oh (email: [email protected])
• Office hours by TAs:
  • Hyoungjin Lim
    • office hour : 5:00pm - 6:00pm Friday in ZOOM
    • https://us02web.zoom.us/j/4705850446?pwd=VllYUzBXR2VNaDhsNytXVytidzByZz09
    • ID: 470 585 0446
    • PW: 567976
  • Dongwoo Oh
    • office hour : 4:00pm - 5:00pm Tuesday in ZOOM
    • https://us04web.zoom.us/j/6081604062?pwd=VFhMeXh1SkRUWHE3NFVpZmx4U0Qvdz09
    • ID: 608 160 4062
    • PW: qJ2SY7

Place and Time

• Place: ZOOM. If the situation of COVID-19 improves substantially, we will use the room 1101 in the E3 building.
• Time: 9:00am - 10:30am on Monday and Wednesday from 31 August 2020 until 16 December 2020.
• Final exam: 12-hour take-home exam on 12 December 2020 (Saturday).

Online Discussion

• We will use KLMS.

3. Homework

Submit your solutions in KLMS. We will create submission folders for all the homework assignments in KLMS.

• Homework1 - Deadline: 6:00pm on 5 October 2020 (Monday).
• Homework2 - Deadline: 6:00pm on 28 October 2020 (Wednesday).
• Homework3 - Deadline: 6:00pm on 25 November 2020 (Wednesday).
• Homework4 - Deadline: 6:00pm on 7 December 2020 (Monday).

4. Tentative Plan

• 08/31 - Introduction and Predicate Logic (Ch1). (slides)
• 09/02 - Predicate Logic (Ch1). (note1, note2, note3, note4, note5, note6, note7, note8, whiteboard1, whiteboard2, whiteboard3)
• 09/07 - Predicate Logic (Ch1). (whiteboard1, whiteboard2, whiteboard3, whiteboard4)
• 09/09 - Predicate Logic (Ch1). (whiteboard1(Sep9), whiteboard2(Sep9), whiteboard3(Sep9), whiteboard4(Sep9), whiteboard1(Sep14), whiteboard2(Sep14))
• 09/14 - The Simple Imperative Language (Ch2). (note1, note2, note3, note4, note5, note6, whiteboard1(Sep14/16), whiteboard2(Sep14/16), whiteboard3(Sep14/16), whiteboard4(Sep14/16))
• 09/16 - The Simple Imperative Language (Ch2).
• 09/21 - The Simple Imperative Language (Ch2). (whiteboard1(Sep21), whiteboard2(Sep21), whiteboard3(Sep21), whiteboard4(Sep21))
• 09/23 - The Simple Imperative Language (Ch2). (whiteboard1(Sep23), whiteboard2(Sep23), whiteboard3(Sep23), whiteboard4(Sep23))
• 09/28 - Program Specification and Their Proofs (Ch3). (note1, note2, note3, note4, whiteboard1(Sep28), whiteboard2(Sep28), whiteboard3(Oct5), whiteboard4(Oct5), whiteboard5(Oct5))
• 09/30 - NO LECTURE. Thanksgiving Day.
• 10/05 - Failure, Input-Output, and Continuation (Ch5). (note1, note2, note3, note4, note5, note6, note7, whiteboard1(Oct5))
• 10/07 - Failure, Input-Output, and Continuation (Ch5). (whiteboard1(Oct7), whiteboard2(Oct7), whiteboard3(Oct7))
• 10/12 - Failure, Input-Output, and Continuation (Ch5). (whiteboard1(Oct12), whiteboard2(Oct12), whiteboard3(Oct12))
• 10/14 - Failure, Input-Output, and Continuation (Ch5). (whiteboard1(Oct14), whiteboard2(Oct14), whiteboard3(Oct14))
• 10/19, 10/21 - NO LECTURES. Midterm Exam.
• 10/26 - Transition Semantics (Ch6). (note1, note2, note3, note4, note5, whiteboard1(Oct26), whiteboard2(Oct26), whiteboard3(Oct26))
• 10/28 - An Introduction to Category Theory (Tennent Ch8). (note1, note2, note3, note4, note5, whiteboard1(Oct28), whiteboard2(Oct28), whiteboard3(Oct28))
• 11/02 - An Introduction to Category Theory (Tennent Ch8). (whiteboard1(Nov2), whiteboard2(Nov2), whiteboard3(Nov2))
• 11/04 - Recursively-Defined Domains (Tennent Ch10). (note1, note2, note3, note4, note5, note6, note7, note8, note9, whiteboard1(Nov4), whiteboard2(Nov4), whiteboard3(Nov4))
• 11/09 - Recursively-Defined Domains (Tennent Ch10). (whiteboard1(Nov9), whiteboard2(Nov9), whiteboard3(Nov9))
• 11/11 - The Lambda Calculus (Ch10). (note1, note2, note3, note4, note5, note6, note7, note8, whiteboard1(Nov11), whiteboard2(Nov11))
• 11/16 - The Lambda Calculus (Ch10). (whiteboard1(Nov16), whiteboard2(Nov16), whiteboard3(Nov16))
• 11/18 - The Lambda Calculus (Ch10). (whiteboard1(Nov18), whiteboard2(Nov18))
• 11/23 - An Eager Functional Language (Ch11). (note1, note2, note3, note4, note5, note6, note7, whiteboard1(Nov23), whiteboard2(Nov23))
• 11/25 - An Eager Functional Language (Ch11). (whiteboard1(Nov25), whiteboard2(Nov25))
• 11/30 - Continuation in a Functional Language (Ch12). (note1, note2, note3, note4, note5, note6, note7, note8, note9, note10, note11, note12, whiteboard1(Nov30), whiteboard2(Nov30))
• 12/02 - Continuation in a Functional Language (Ch12). (whiteboard1(Dec2), whiteboard2(Dec2), whiteboard3(Dec2))
• 12/07 - Q&A Session. (whiteboard1(Dec7), whiteboard2(Dec7), whiteboard3(Dec7))
• 12/09 - NO LECTURE. KAIST Undergraduate Admission.
• 12/14, 12/16 - NO LECTURES. Final Exam.

5. Studying Materials

We will mainly follow Reynolds's book, but study the materials appearing in Chapters 8 and 10 of Tennent's book.

• Main Textbook 1 : Theories of Programming Languages, John C Reynolds, Cambridge University Press, 1998.
• Main Textbook 2 : Semantics of Programming Languages, Robert D. Tennent, Prentice Hall, 1991. Chapters 8 and 10 only.

In addition to the two books above, the following books will have further information about the topics covered in the course. In particular, Gunter's book goes deep into the domain theory, and Pierce's book into the type theory.

• Auxiliary Textbook 1 : Semantics of Programming Languages: Structures and Techniques, Carl A. Gunter, MIT Press, 1992.
• Auxiliary Textbook 2 : Types and Programming Languages, Benjamin C. Pierce, MIT Press, 2002.
• Auxiliary Textbook 3 : Formal Semantics of Programming Languages: an Introduction, Glynn Winskel, MIT Press, 1993.

The following classic papers or their recent reprints contain deep insight into some of topics that we study throughout the course.

• John C. Reynolds, Definitional Interpreters for Higher-Order Programming Languages, Higher-Order and Symbolic Computation, 1998.
• Luis Damas and Robin Milner, Principal Type-Schemes for Functional Programs, POPL 1982.

5. Two Critical Surveys

One important part of this course is to study assigned topics for yourself, and write surveys about them, which also contain critiques or original thoughts of the student. It accounts for the 30% of the total marks of this course. In order to get full marks, a student has to show in his or her write-up that she or he has understood the topics well, carried out in-depth studies on the topics, and thought hard and originally about them. Our evaluation adopts the following criterion: the clarity of writing (20%), the level of understanding a topic and existing work about it (40%), and the demonstration of original thoughts and insights (40%). Here are the details of this assignments.

1. Don't postpone this assignments until the last moment.
2. There are two assignments. In both cases, a submission should be at most 3 pages not including bibliography.
3. First assignment:
   1. Topic: Concurrent separation logic.
   2. Deadline: 23:59 of the 30th of October in 2020 (Friday). Summit in KLMS.
   3. Some references that may help you to start:
      1. Peter O'Hearn. Resources, Concurrency, and Local Reasoning. This is the paper that started concurrent separation logic.
      2. Stephen Brookes and Peter O'Hearn. Concurrent Separation Logic.
      3. Peter O'Hearn. Separation Logic.
      4. Peter O'Hearn, John Reynolds, and Hongseok Yang. Local Reasoning about Programs that Alter Data Structures. This paper describes one of the key ideas behind separation logic, called local reasoning.
      5. Stephen Brookes. A Semantics for Concurrent Separation Logic.
   4. Questions to think about:
      1. What is separation logic? What is concurrent separation logic?
      2. Which aspects of concurrent separation logic help construct the proofs of concurrent programs more easily?
      3. What recent research results result from concurrent separation logic?
      4. Can you find a new application where concurrent separation logic or its key ideas can be applied?
      5. How would you improve concurrent separation logic?
      6. If you want to show the termination (more generally liveness properties), how should you extend concurrent separation logic?
4. Second assignment.
   1. Topic: Relational parametricity.
   2. Deadline: 23:59 of the 7th of December in 2020 (Monday). Summit in KLMS.
   3. Some references that may help you to start:
      1. John Reynolds. Types, Abstraction and Parametric Polymorphism..
      2. Philip Wadler. Theorems for free!.
      3. Chapter 17 of the textbook by Reynolds.
      4. John Reynolds. An Introduction to Polymorphic Lambda Calculus.
      5. The above papers are classic papers on this topic. I suggest you to have a look at more recent papers on this topic as well, published in PL conferences and journals such as POPL, LICS, MFPS, TOPLAS.
   4. Questions to think about:
      1. What is polymorphism?
      2. How parametric polymorphism and ad-hoc polymorphism differ and get realised in programming languages?
      3. How relational parametricity formalises parametric polymorphism?
      4. What are the consequences of relational parametricity for properties of programs?
      5. How does relational parametricity relate to other programming language concepts such as data abstraction?
      6. Can you find a new way of using the key idea behind relational parametricity?
      7. What do researchers work on relational parametricity nowadays?