This course provides students with a foundational understanding of software theory. As software verification and testing become
increasingly critical for ensuring system correctness, a strong grasp of these theoretical underpinnings is essential. Furthermore,
the course offers key conceptual frameworks for language design, providing students with methodological insights for developing
new programming languages in the future.
This course covers the fundamental aspects of software theory, with a particular focus on inductive definitions and induction
--- essential concepts for the formal treatment of programs. We will also explore type systems for programming languages,
whose utility has become increasingly recognized in recent years, as well as program semantics.
Specifically, the course will:
- explain well-founded induction and demonstrate how mathematical induction and structural induction are specific instances of this broader principle.
- present and analyze concrete type systems, focusing on the core components of both functional and object-oriented languages.
- primarily discuss operational semantics, targeting Boolean expressions and the essential structures of functional and object-oriented programming.
Specifically, the course will:
- explain well-founded induction and demonstrate how mathematical induction and structural induction are specific instances of this broader principle.
- present and analyze concrete type systems, focusing on the core components of both functional and object-oriented languages.
- primarily discuss operational semantics, targeting Boolean expressions and the essential structures of functional and object-oriented programming.
- To be able to define a set inductively and to prove inductively simple properties about the set.
- To be able to show that a given short program is consistent with respect to a given type system.
- To be able to show the semantics of a given short program when given an operational semantics for the language.
| mid-term exam | final-exam | Total. | |
|---|---|---|---|
| 1. | 10% | 10% | 20% |
| 2. | 20% | 20% | 40% |
| 3. | 20% | 20% | 40% |
| Total. | 50% | 50% | - |
| Class schedule | HW assignments (Including preparation and review of the class.) | Amount of Time Required | |
|---|---|---|---|
| 1． | Inductive definition of sets | Reference book [1] | 180minutes |
| 2． | Inductive proof - well-founded induction |
Reference book [1] | 190minutes |
| 3． | Inductive proof - structural induction |
Reference book [1] | 190minutes |
| 4． | Inductive proof - induction for derivation tree |
Reference book [1] | 190minutes |
| 5． | Operational semantics - a simple language (boolean expressions) |
Reference book [2] | 190minutes |
| 6． | An example of proof of properties about boolean expressions | Reference book [2] | 190minutes |
| 7． | Mid-term examination and its explanation - written examination about the contents from the 1st to 7th lectures. (We resume the lecture after the mid-term examination.) |
Review everything until the last time. | 190minutes |
| 8． | Operational semantics - a type system for a simply-typed lambda calculus |
Reference book [2] | 190minutes |
| 9． | Type system - a type system for a simply-typed lambda calculus |
Reference book [2] | 190minutes |
| 10． | Operational semantics - operational semantics for functional languages having various constructs |
Reference book [2] | 190minutes |
| 11． | Type system - type systems for functional languages having various constructs |
Reference book [2] | 190minutes |
| 12． | Operational semantics - an operational semantics of a simple object-oriented language ”Featherweight Java” |
Reference book [2] | 190minutes |
| 13． | Type system - a type system of Featherweight Java |
Reference book [2] | 190minutes |
| 14． | Final examination and its explanation - written examination about the contents from the 1st to 14th lectures. |
Review everything until the last time. | 190minutes |
| 15． | |||
| Total. | - | - | 2650minutes |
Let the mid-term exam go up to 50 and the final exam go up to 50. Then the total score is M+F*(100-M)/50 when the scores of
the mid-term and the final exams are M and F respectively.
If you can solve problems about type judgement and operational semantics concerning simple languages presented in this class, you are in the level of obtaining 60-point.
If you can solve problems about type judgement and operational semantics concerning simple languages presented in this class, you are in the level of obtaining 60-point.
| ways of feedback | specific contents about "Other" |
|---|---|
| Feedback in the class |
References:
[1] Glynn Winskel, The Formal Semantics of Programming Languages --- An Introduction, The MIT Press, 1993.
[2] Benjamin C. Pierce, Types and Programming Langauges, The MIT Press, 2002.
[1] Glynn Winskel, The Formal Semantics of Programming Languages --- An Introduction, The MIT Press, 1993.
[2] Benjamin C. Pierce, Types and Programming Langauges, The MIT Press, 2002.
A foundational understanding of programming languages is essential for this course. It is assumed that students possess knowledge
equivalent to the "Principles of Programming Languages" course offered to second-year undergraduates in the Department of
Computer Science and Engineering.
While this course covers more fundamental theoretical aspects and does not strictly require prior credit in "Principles of Programming Languages," students will likely find the material difficult to follow without a solid background in the subject. Students from other departments who find the "Course content" difficult to comprehend should be prepared to dedicate a significant amount of additional time to self-study.
While this course covers more fundamental theoretical aspects and does not strictly require prior credit in "Principles of Programming Languages," students will likely find the material difficult to follow without a solid background in the subject. Students from other departments who find the "Course content" difficult to comprehend should be prepared to dedicate a significant amount of additional time to self-study.
- Thursday 12:30-12:40 or any time agreed on by email via zoom
- Course that cultivates a basic problem-solving skills
| Work experience | Work experience and relevance to the course content if applicable |
|---|---|
| N/A | N/A |
Last modified : Sat Mar 14 14:26:33 JST 2026