This course provides foundations for software, such as an inductive definition of a set and an inductive proof which is useful
in treating programs formally, type systems of programming languages whose usefulness have been gradually recognized, and
semantics of programming languages. As for inductive proofs we introduce the well-founded induction and then show that mathematical
inductions and structural inductions are its instances. As for type systems we show simple type systems for cores of functional
and object-oriented languages. As for semantics we mainly show operational semantics for boolean expressions and cores of
functional and object-oriented languages.
By taking this class students will obtain foundations for programming languages.
This kind of foundations underlie program verification or testing.
Also in the future they may engaged in developing a new language, in such cases this kind of foundations may indirectly help them to consider what kind of things they should take into account.
This kind of foundations underlie program verification or testing.
Also in the future they may engaged in developing a new language, in such cases this kind of foundations may indirectly help them to consider what kind of things they should take into account.
- 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.
It is essential to have a basic understanding of programming languages. It is assumed to have knowledge equivalent to that
taught in the "Principles of Programming Languages" course, which is offered to second-year students in the Department of
Computer Science and Engineering at this university. Although the content of this class is more fundamental than the university’s
"Principles of Programming Languages" course, and such knowledge is not strictly required in principle, in practice, it is
likely to be difficult to understand the course material without a certain level of knowledge about programming languages.
- 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 : Tue Oct 08 04:03:49 JST 2024