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 cores of imperative, 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.
| 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 imperative language |
Reference book [2] | 190minutes |
| 6． | An example of proof of properties about programs of the simple imperative language | 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 |
| mid-term exam | final-exam | Total. | |
|---|---|---|---|
| 1. | 10% | 10% | 20% |
| 2. | 20% | 20% | 40% |
| 3. | 20% | 20% | 40% |
| Total. | 50% | 50% | - |
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.
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.
[3] John C. Mitchell, Foundations for Programming Languages, The MIT Press, 1996.
[4] John C. Mitchell, Concepts in Programming Languages, Cambridge University Press, 2002.
[5] Ravi Sethi, Programming Languages --- Concepts & Constructs 2nd edition, Addison Wesley, 1996.
[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.
[3] John C. Mitchell, Foundations for Programming Languages, The MIT Press, 1996.
[4] John C. Mitchell, Concepts in Programming Languages, Cambridge University Press, 2002.
[5] Ravi Sethi, Programming Languages --- Concepts & Constructs 2nd edition, Addison Wesley, 1996.
Basic knowledge of programming languages is required, hopefully the knowledge studied in the course about the programming
languages for the 2nd year undergraduate students of the department of information science and engineering.
Last modified : Fri Oct 06 05:21:22 JST 2017