Security Types Preserving Compilation
手続き呼び出しの書ける低レベル言語を対象に非干渉性に関して健全な情報流解析のための型システムを提案。さらに情報流解析のための型システムによって型付け可能な高レベル言語から型付け可能な低レベル言語へのコンパイルを定義。
author="Gilles Barthe and Tamara Rezk and Amitabh Basu",
title="{Security Types Preserving Compilation}",
journal="Computer Languages, Systems and Structures",
volumn="33",
number="2",
pages="35--59",
year="2007"
Union Types for Object-Oriented Programming
union type の提案。union type は 2 つのクラスの同じ名前のメンバに関しては区別なく扱えるような型のこと。S と T の union type を (S or T) と書くことにして、D1 と D2 が C を継承して E1 が D1 を、E2 が D2 を継承しているとすると、E1 と E2 は (E1 or E2) の subtype で、D1, D2, (E1 or E2) は (D1 or D2) の subtype で、(D1 or D2) は C の subtype となる。あと、union type な式に対して具体的な値の型で分岐する case 文を導入。意味論と型付け規則を定義して健全性を証明。
author="Atsushi Igarashi and Hideshi Nagira",
title="{Union Types for Object-Oriented Programming}",
booktitle="SAC '06",
publisher="ACM",
pages="1435--1441",
year="2006"
本
- コード・クラフト : エクセレントなコードを書くための実践的技法
- Goodliffe, Pete，鵜飼, 文敏，後藤, 正徳，平林, 俊一, 1971-，トップスタジオ 著
- 毎日コミュニケーションズ
ようやく読了。買ったのは出版されてすぐだったから 2 年たってる。
本
- ソフトウエア・クリエイティビティ : ソフトウエア開発に創造性はなぜ必要か
- Glass, Robert L, 1932-，高嶋, 優子，徳弘, 太郎，森田, 創 著
- 日経BP出版センター
読了。