/graduatePL19

CS520 Theory of Programming Languages, Fall 2019, 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 2019. 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

[13 December] Model answers for HW4, HW5 will be distributed.

Some students asked about model answers for homework. We will distribute the model answers for HW4, HW5 in hard copies during the office hour next week (room 3431, E3-1, 16 Dec from 3:00PM to 5:00PM). However, We won't give the model answers for HW1~3, and any model answers will not be distributed online.

[9 December] Reminder of the final exam.

As announced before, the final exam will take place at our lecture room (room 112, N1) from 9:00am until 11:00am on 18 December 2019 (Wednesday). It is a closed-book exam, and it covers all the materials discussed in the lectures. The questions will be in a style similar to the homework exercises.

[1 December] The due date for the second critical review is approaching.

As announced in the beginning of this course, the deadline for the second critical review is the midnight of the 9th of December in 2019 (Monday). To write a sensible review, you will have to study not a small amount of materials. So, make sure that you start this assignment early enough.

[1 December] Homework5 is out.

You don't have to submit your answers. In fact, even if you submit something, we won't mark it. But I strongly recommend you to try the questions in the homework, at least before the final exam.

[17 November] Homework4 is out.

The fourth homework is out. The deadline is 2:00pm on the 4th of December 2019 (Wednesday). Submit your solutions to the TAs by putting them in the homework submission box in the third floor of the E3-1 building. If you type up your solutions, you can submit them via KLMS.

[27 October] The due date for the first critical review is approaching.

The due date for the first critical review is the midnight on 1 November 2019 (Friday). Your review should be three pages or less. Make sure that you submit something even if your write-up is not as good as you want. As usual, you can submit your review in the CS520 homework submission box in the third floor of the E3-1 building, or electronically via KLMS.

[27 October] Homework3 is out.

The third homework is out. The deadline is 2:00pm on the 15th of November 2019 (Friday). Submit your solutions to the TAs by putting them in the homework submission box in the third floor of the E3-1 building. If you type up your solutions, you can submit them via KLMS.

[13 October] Homework2 is out.

The second homework is out. The deadline is 2:00pm on the 30th of October 2019 (Wednesday). Submit your solutions to the TAs by putting them in the homework submission box in the third floor of the E3-1 building. If you type up your solutions, you can submit them via KLMS.

[22 September] Homework1 is out.

The first homework is out. The deadline is 2:00pm on the 4th of October 2019 (Friday). Submit your solutions to the TAs by putting them in the homework submission box in the third floor of the E3-1 building. If you type up your solutions, you can submit them via KLMS.

[5 September] Room change

From the lecture on 9 September (Monday), we will meet at the room 112 in the N1 building. Also, the final exam will take place at the room 112 as well.

2. Logistics

Evaluation

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

Teaching Staffs

Place and Time

  • Place: room 112 in the N1 building
  • Time: 10:30am - 11:45am on Monday and Wednesday from 2 September 2019 until 20 December 2019.
  • Final exam: 9:00am - 11:00am on 18 December 2019 (Wednesday) at the room 112 in the N1 building.

Online Discussion

  • We will use KLMS.

3. Homework

Submit your solutions by putting them in the homework submission box in the third floor of the E3-1 building, or uploading your solutions on KLMS.

4. Tentative Plan

  • 09/02 - Introduction (slides). Predicate Logic (Ch1) (note1, note2, note3, note4, note5, note6, note7, note8).
  • 09/04 - Predicate Logic (Ch1).
  • 09/09 - Predicate Logic (Ch1).
  • 09/11 - Predicate Logic (Ch1).
  • 09/16 - The Simple Imperative Language (Ch2) (note1, note2, note3, note4, note5, note6).
  • 09/18 - The Simple Imperative Language (Ch2).
  • 09/23 - The Simple Imperative Language (Ch2).
  • 09/25 - The Simple Imperative Language (Ch2).
  • 09/30 - Program Specification and Their Proofs (Ch3). (note1, note2, note3, note4).
  • 10/02 - Program Specification and Their Proofs (Ch3).
  • 10/07 - Failure, Input-Output, and Continuation (Ch5). (note1, note2, note3, note4, note5, note6, note7).
  • 10/09 - NO LECTURE. Hangle Proclamation Day.
  • 10/14 - Failure, Input-Output, and Continuation (Ch5).
  • 10/16 - Failure, Input-Output, and Continuation (Ch5).
  • 10/21, 10/23 - NO LECTURES. Midterm Exam.
  • 10/28 - Transition Semantics (Ch6). (note1, note2, note3, note4, note5).
  • 10/30 - An Introduction to Category Theory (Tennent Ch8). (note1, note2, note3, note4, note5).
  • 11/04 - An Introduction to Category Theory (Tennent Ch8).
  • 11/06 - Recursively-Defined Domains (Tennent Ch10). (note1, note2, note3, note4, note5, note6, note7, note8, note9).
  • 11/11 - Recursively-Defined Domains (Tennent Ch10).
  • 11/13 - Recursively-Defined Domains (Tennent Ch10).
  • 11/18 - The Lambda Calculus (Ch10). (note1, note2, note3, note4, note5, note6, note7, note8).
  • 11/20 - The Lambda Calculus (Ch10).
  • 11/25 - The Lambda Calculus (Ch10).
  • 11/27 - NO LECTURE. KAIST Undergraduate Admission.
  • 12/02 - An Eager Functional Language (Ch11). (note1, note2, note3, note4, note5, note6, note7).
  • 12/04 - An Eager Functional Language (Ch11).
  • 12/09 - Continuation in a Functional Language (Ch12). (note1, note2, note3, note4, note5, note6, note7, note8, note9, note10, note11, note12).
  • 12/11 - Continuation in a Functional Language (Ch12).
  • 12/16 12/18 - 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.

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.

5. Two Critical Reviews

One important part of this course is to study assigned reading materials and write reviews about them. 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 thought hard about the materials and gone beyond the simple understanding of them. Here are the details of this assignments.

  1. There are two assignments for this critical review.
  2. First assignment:
    1. Topic: Shared-variable concurrency.
    2. Deadline: midnight of the 1st of November in 2019 (Friday).
    3. Reading material: Chapter 8 of Reynolds's ''Theories of Programming Languagues.'' This chapter is about shared-variable concurrency. To understand the chapter, you may have to know some materials in Chapter 7, which is about nondeterminism and guarded commands.
  3. Second assignment.
    1. Topic: ML type inference.
    2. Deadline: midnight of the 9th of December in 2019 (Monday).
    3. References:
      1. Francois Pottier, A Modern Eye on ML Type Inference, September, 2005.
      2. Luis Damas and Robin Milner, Principal Type-Schemes for Functional Programs, POPL 1982.
      3. (Optional) Francois Pottier and Didier Remy, The Essence of ML Type Inference, Chapter 10, Advanced Topics in Types and Programming Languages. An extended version of the paper and a prototype implementation are available here.
  4. A review should have three pages or less.