AAA551: Programming Language Theory, 2026 Spring
Course Information
- Instructor: Jihyeok Park (박지혁)
- Office: 507, IT & General Education Center (정운오IT교양관)
- Email: jihyeok_park@korea.ac.kr
- Lecture: 13:30–14:45 Tuesday and Thursday @ 519, IT & General Education Center (정운오IT교양관)
- Office hours: 14:00–16:00 Tuesdays (by appointment)
Course Materials
- Self-contained lecture notes are provided.
- Reference:
- Types and Programming Language by Benjamin C. Pierce.
- Advanced Topics in Types and Programming Languages by Benjamin C. Pierce.
- Itroduction to Static Analysis: An Abstract Interpretation Perspective by Xavier Rival and Kwangkeun Yi.
Grading
Please use the LMS for the attendance check and the submission of homework.
- Homework: 80%
- Attendance: 20%
Installation of Scala and sbt
Scala is a general-purpose programming language combining object-oriented and functional programming in one concise, high-level language. Scala’s static types help avoid bugs in complex applications, and its JVM and JavaScript runtimes let you build high-performance systems with easy access to huge ecosystems of libraries.
The interactive build tool sbt is built for Scala and Java projects.
Please download and install them using the following links:
- JDK >= 17 - https://www.oracle.com/java/technologies/downloads/
- sbt - https://www.scala-sbt.org/download.html
- Scala - https://www.scala-lang.org/download/
Schedule
| # | Date | Title | Homework | |||
|---|---|---|---|---|---|---|
| 0 | 03/03 | Course Overview | ||||
| 1 | 03/05 | Basic Introduction to Scala | ex01 | |||
| Part 1: Semantics | ||||||
| 2 | 03/10 | Big-Step Operational Semantics | ||||
| 3 | 03/12 | Small-Step Operational Semantics | ||||
| 4 | 03/17 | Evaluation Context and Lambda Calculus | ||||
| 5 | 03/19 | Denotational Semantics | ||||
| 6 | 03/24 | Fixed-Point Theory | ||||
| 7 | 03/26 | Trace Semantics | ||||
| 8 | 03/31 | Trace Properties | ||||
| 9 | 04/02 | Abstract Machines | hw01 (by 04/16) | |||
| 10 | 04/07 | Axiomatic Semantics | ||||
| 11 | 04/09 | Systematic Program Proofs | ||||
| 12 | 04/14 | Separation Logic (1) | ||||
| 13 | 04/16 | Separation Logic (2) | ||||
| Part 2: Type System | ||||||
| 14 | 04/28 | Type System | ||||
| 15 | 04/30 | Simply-Typed Lambda Calculus | ||||
| 16 | 05/05 | Type Extensions | ||||
| 17 | 05/07 | Universal Types | ||||
| 18 | 05/12 | Subtyping | ||||
| 19 | 05/14 | Existential Types | ||||
| 20 | 05/19 | Type Operators | ||||
| 21 | 05/21 | Curry-Howard Isomorphism | ||||
| 22 | 05/26 | Dependent Types | ||||
| 23 | 05/28 | Calculus of Constructions | ||||
| 24 | 06/02 | Flow-Sensitive Types | hw02 (by 06/09) | |||
| 25 | 06/04 | Substructural Types | ||||
| 26 | 06/09 | Effect Systems | ||||
| 27 | 06/11 | Course Review | ||||