Course title
1M9882001
Software Construction

sasano isao Click to show questionnaire result at 2018
Course content
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.
Purpose of class
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.
Goals and objectives
  1. To be able to define a set inductively and to prove inductively simple properties about the set.
  2. To be able to show that a given short program is consistent with respect to a given type system.
  3. To be able to show the semantics of a given short program when given an operational semantics for the language.
Language
Japanese
Class schedule

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
Relationship between 'Goals and Objectives' and 'Course Outcomes'

mid-term exam final-exam Total.
1. 10% 10% 20%
2. 20% 20% 40%
3. 20% 20% 40%
Total. 50% 50% -
Evaluation method and criteria
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.
Textbooks and reference materials
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.
Prerequisites
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.
Office hours and How to contact professors for questions
  • Friday 13:10-14:50 or any time agreed on by email
Relation to the environment
Non-environment-related course
Regionally-oriented
Non-regionally-oriented course
Development of social and professional independence
  • Course that cultivates a basic problem-solving skills
Active-learning course
More than one class is interactive
Course by professor with work experience
Work experience Work experience and relevance to the course content if applicatable
N/A N/A
Last modified : Thu Mar 21 15:32:07 JST 2019