This is a webpage of the course "CS520 Theory of Programming Languages", which is offered at the KAIST CS department in the fall of 2024. 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.
[23 November] Homework3 is out.
The third homework assignment is out. Submit your solutions in KLMS by 6:00pm on 9 December 2024 (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.
[29 October] Homework2 is out.
The second homework assignment is out. Submit your solutions in KLMS by 6:00pm on 8 November 2024 (Friday).
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.
[1 October] Homework1 is out.
The homework assignment 1 is out. Submit your solutions in KLMS by 6:00pm on 18 October 2024 (Friday).
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.
The first of October is a national holiday. We won't have a class on that day.
We strongly recommend students to ask questions in KLMS, instead of in github, if they have any. This would help fellow students to access those questions and corresponding answers more easily. It would also help TAs and the lecturer not to miss those questions.
We do not permit students to ask homework questions directly to ChatGPT, Gemini, or other LLMs. Doing so would be regarded as the violation of the honour code. However, students can use LLMs to get help for their study, for instance, using CoPilot to solve LaTeX typesetting issues and asking ChatGPT to get an overview of a concept or a technique covered in the course or encountered in your group project. If a student or a project group gets help from LLMs for an assignment, such as a project report, the student or the group should do the following two things:
- In a submission, the student or the project group should explain how and where LLMs are used.
- LLMs are well-known to give false information. Ensuring correctness is the responsibility of the student or the project group.
We will adopt the following scheme for handling late submissions for all types of assignments, including homework assignments. The scheme assumes that the total marks are 100.
- <= One day late (by the midnight of the next day): -10
- <= Two days late: -20
- <= Three days late: -30
- <= Four days late: -40
- More than four days late: -100.
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 any assignment, he or she will get F.
We also handle the case of plagiarism strictly. Plagiarism means that students copy texts from other sources in their reports. They shouldn't do it. If students have to use texts from other sources, they have to rephrase the texts in their own words and state the source of the texts explicitly. Ideally, students' write-ups should mostly consist of their own phrases and expressions, and use such borrowed and rephrased sentences only when doing so is absolutely needed; if a large part of the report is just a series of rephrases of existing texts, the report won't get good marks. Copying texts from other sources is an instance of plagiarism, and if it happens to an academic, it can destroy his or her research career. If a report of a student or a project group is found to plagiarise, the student or everyone in the group will get F.
- Final exam (40%). Group project (40%). Homework (20%).
- Lecturer: Prof Hongseok Yang (email: hongseok00@gmail.com, office hour: 6:00pm - 7:00pm on Monday, office: 3403 in E3-1.)
- TAs: Gyeongwon Jung (email: jgyw0910@kaist.ac.kr) and Sangho Lim (email: lim.sang@kaist.ac.kr), office hour: 4:00pm - 5:00pm on Tuesday, office: 3419 in E3-1.
- Time: 14:30 - 16:00 on Tuesday and Thursday.
- Place: 1101 in E3.
The final exam for this course will happen in our usual classroom on the 19th of December (Thursday) during the final-exam period. Note that the exam starts at 1:00pm.
- Date: 19 December 2024 (Thursday).
- Time: 13:00 - 14:30.
- Place: 1101 in E3.
- Closed-book exam. The scope of the exam is all the topics covered in the classes.
One important part of this course is to form a group of 2-4 students, study an advanced research topic on programming languages with fellow students in the group, and present what the group studied if the group is selected for presentation. Here are the detailed instructions on this group project.
- Form a group.
- Deadline - 11:59PM on 26 September 2024 (Thursday).
- Form a group with 2-4 students.
- Select a topic and write a proposal (5 marks out of 40 marks).
- Deadline - 11:59PM on 17 October 2024 (Thursday).
- Pick a paper or papers on the theories of programming languages that will be studied by your group. The paper or papers should be chosen among papers published in POPL'20, POPL'21, POPL'22, POPL'23, POPL'24, PLDI'20, PLDI'21, PLDI'22, PLDI'23, and PLDI'24.
- Submit a 1-page proposal in KLMS that contains the title(s) of the selected paper(s), the reasoning for choosing it or them, and the plan to study the paper in depth.
- The proposal can be submitted by only one member of each team.
- Write a report (15 marks out of 40 marks).
- Deadline - 11:59PM on 21 November 2024 (Thursday).
- Submit a report with at most 4 pages excluding bibliography and figures in KLMS.
- The report can be submitted by only one member of each team.
- The report should explain not just the topic studied by your group but also how the group studied the topic. The latter can be about how the group members studied the topic together, which questions they asked in order to understand the topic in depth, which other papers they studied, which existing implementations or mechanised proofs they looked at if there are any such, and how each member of the group contributed to the study, etc.
- We encourage the students to go beyond a simple summary of the topic, and to have their own thoughts on the topic in the form of mathematical or experimental analyses. For instance, if the existing results on a chosen topic mostly use the call-by-value setting, the students may try to find out which parts of the results survive in the call-by-name setting.
- Submit the slides of a presentation on the studied topic (15 marks out of 40 marks).
- Deadline - 11:59PM on 28 November 2024 (Thursday).
- Prepare the slides for a 35-minute talk on the studied topic, and submit them in KLMS.
- The slides can be submitted by only one member of each team.
- The slides should be in the pdf format.
- Present your study if your group project is chosen (5 marks out of 40 marks).
- Four projects will be selected based on the votes by the students, TAs, and the lecturer.
- Two projects will be presented on 10 December 2024 (Tuesday), and the other two will be presented on 12 December 2024 (Thursday).
- Warning on plagiarism.
- Students should not copy texts from other sources in their reports. If students have to use such texts, they have to rephrase the texts in their own words and state the source of the texts explicitly. Ideally, students' write-ups should mostly consist of the students' own phrases and expressions, and use such borrowed and rephrased sentences only when doing so is absolutely needed. Copying texts from other sources is an instance of plagiarism, and if it happens to an academic, it can destroy his or her research career. If any of the reports of a group is found to plagiarise, everyone in the group will get F.
Submit your solutions in KLMS. We will create submission folders for all the homework assignments in KLMS.
- Homework1 - Deadline: 6:00pm on 18 October 2024 (Friday).
- Homework2 - Deadline: 6:00pm on 8 November 2024 (Friday).
- Homework3 - Deadline: 6:00pm on 9 December 2024 (Monday).
- 09/03(Tue) - Introduction.
- 09/05(Thu) - Predicate Logic (Ch1).
- 09/10(Tue) - Predicate Logic (Ch1).
- 09/12(Thu) - Predicate Logic (Ch1).
- 09/17(Tue) - NO LECTURE. Chuseok.
- 09/19(Thu) - Predicate Logic (Ch1).
- 09/24(Tue) - The Simple Imperative Language (Ch2).
- 09/26(Thu) - The Simple Imperative Language (Ch2).
- 10/01(Tue) - NO LECTURE. National Foundation Day.
- 10/03(Thu) - NO LECTURE. National Foundation Day.
- 10/08(Tue) - The Simple Imperative Language (Ch2).
- 10/10(Thu) - The Simple Imperative Language (Ch2).
- 10/15(Tue) - Program Specification and Their Proofs (Ch3).
- 10/17(Thu) - Program Specification and Their Proofs (Ch3).
- 10/22(Tue) - NO LECTURES. Week for Mid-term Exams.
- 10/24(Thu) - NO LECTURES. Week for Mid-term Exams.
- 10/29(Tue) - Failure, Input-Output and Continuation (Ch5).
- 10/31(Thu) - Failure, Input-Output and Continuation (Ch5).
- 11/05(Tue) - Failure, Input-Output and Continuation (Ch5).
- 11/07(Thu) - Failure, Input-Output and Continuation (Ch5).
- 11/12(Tue) - Failure, Input-Output and Continuation (Ch5).
- 11/14(Thu) - Failure, Input-Output and Continuation (Ch5).
- 11/19(Tue) - Transition Semantics (Ch6)
- 11/21(Thu) - The Lambda Calculus (Ch10).
- 11/26(Tue) - The Lambda Calculus (Ch10).
- 11/28(Thu) - NO LECTURES. Interview for Undergraduate Admission.
- 12/03(Tue) - An Eager Functional Language (Ch11).
- 12/05(Thu) - An Eager Functional Language (Ch11)
- 12/10(Tue) - Project Presentations.
- 12/12(Thu) - Project Presentations.
- 12/17(Tue) - NO LECTURES. Week for Final Exams.
- 12/19(Thu) - FINAL EXAM (1:00pm - 2:30pm, 1101 E3).
The lectures will be based on the following hand-written notes, which summarise the contents of the two main textbooks. Reading these notes and solving exercises in the notes is a recommended way to study the topics covered by the course.
- Predicate Logic (Ch1) (note1, note2, note3, note4, note5, note6, note7, note8).
- The Simple Imperative Language (Ch2) (note1, note2, note3, note4, note5, note6).
- Program Specification and Their Proofs (Ch3) (note1, note2, note3, note4).
- Failure, Input-Output, and Continuation (Ch5) (note1, note2, note3, note4, note5, note6, note7).
- Transition Semantics (Ch6) (note1, note2, note3, note4, note5).
- An Introduction to Category Theory (Tennent Ch8) (note1, note2, note3, note4, note5).
- Recursively-Defined Domains (Tennent Ch10) (note1, note2, note3, note4, note5, note6, note7, note8, note9).
- The Lambda Calculus (Ch10) (note1, note2, note3, note4, note5, note6, note7, note8).
- An Eager Functional Language (Ch11) (note1, note2, note3, note4, note5, note6, note7).
- Continuation in a Functional Language (Ch12) (note1, note2, note3, note4, note5, note6, note7, note8, note9, note10, note11, note12).
We will mainly follow Reynolds's book, and we may cover 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, Harper's book goes deep into the type systems and operational semantics of a range of programming languages, Gunter's book into the domain theory, and Pierce's book into the type theory.
- Auxiliary Textbook 1 : Practical Foundations for Programming Languages, Second Edition, Robert Harper, Cambridge University Press, 2016.
- Auxiliary Textbook 2 : Semantics of Programming Languages: Structures and Techniques, Carl A. Gunter, MIT Press, 1992.
- Auxiliary Textbook 3 : Types and Programming Languages, Benjamin C. Pierce, MIT Press, 2002.
- Auxiliary Textbook 4 : 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.