Object and Reference Immutability using Java Generics
object immutability と reference immutability を Java の generics を使って実現する方法の提案。不変性を表すために Immutable, Mutable, ReadOnly の 3 つの要素を用意し、一種のクラスのように扱う。正しいプログラムのためのルールを定義し、型システムとして定式化。mutable reference は mutable object を指すことと immutable reference は immutalbe object を指すことに対して健全であることを証明。
author="Yoav Zibin and Alex Potanin and Mahmood Ali and Shay Artzi and Adam Kie{\.z}un and Michael D. Ernst",
title="{Object and Reference Immutability using Java Generics}",
booktitle="ESEC/FSE 2007",
publisher="ACM Press",
pages="75--84",
year="2007"
Searching for Type-Error Messages
前読んだ論文の発展版。同一関数内に複数型エラーがある場合に対応したり、評価したり、C++ に応用したりしている。
author="Benjamin S. Lerner and Matthew Flower and Dan Grossman and Craig Chambers",
title="{Searching for Type-Error Messages}",
booktitle="PLDI 2007",
publisher="ACM Press",
pages="425--434",
year="2007"
Immutable Objects for a Java-Like Language
オブジェクトが immutable かどうか検査する型システムの提案。read-only かどうか、owner が誰か、などを記述する。あと、コンストラクタ内でのみ mutable であること、コンストラクタが this を外部に見せないことなども要請。Javari は参照の immutability を検査するけど、こっちは参照ではなくオブジェクトなのが違う。
author="Christian Haack and Erik Poll and Jan Schäfer and Aleksy Schubert",
title="{Immutable Objects for a Java-Like Language}",
booktitle="Proceedings of the 16th European Symposium on Programming",
publisher="Springer",
volume="4421",
series="LNCS",
pages="347--362",
year="2007"
A Type Safe DOM API
DOM API に対する型システムの提案。Java の型システムを拡張する形で定義。属性ノードは高々一つの要素に属するとか、要素と属性は同じドキュメントに由来するとか、そういった制約を型付け規則として記述する。意味も定義して健全性が示されている。
author="Peter Thiemann",
title="{A Type Safe DOM API}",
booktitle="DBPL 2005",
publisher="Springer",
volume="3774",
series="LNCS",
pages="169--183",
year="2005"
SEMINAL: Searching for Error Messages in Advanced Languages
型エラーが発生したら構文木を「適当に」変更して型付け可能か調べ、型付け可能になるような変更をユーザに提示する手法の提案。構文木をどう変更するか、見つけた変更をどう提示するか、といったあたりが中心。
author="Benjamin Lerner and Dan Grossman and Craig Chambers",
title="{SEMINAL: searching for ML type-error messages}",
booktitle="ML'06",
publisher="ACM Press",
pages="63--73",
year="2006"