2 0 0 0 OA Rubyに対するGradual typingの導入
プログラミング言語Rubyは,広く使用されている動的型付け言語である. Rubyは実行時に型チェックを行うため,プログラムを実行し型エラーを含む部分に実行が及ばなければ型エラーは報告されない. このことは,プログラム中に型エラーによるバグが潜在的に残り,バグの発見が遅れたり,バグを見逃したりする要因となっている. このような動的型付けの欠点を補う方法として,Gradual typingが提案されている. Gradual typingとは,型注釈の有無により型付けの手法が異なるような型システムである. 型注釈がある部分については静的に型付けをし,実行前に型チェックを行う. 型注釈がない部分については動的型として型付けをし,実行時に型チェックを行う. 本研究の目的は,Rubyの動的型付けによる柔軟性を残しつつ,プログラムの型エラーによるバグの発見を容易にすることである. その方針として,RubyにGradual typingを導入することで,静的型エラーの検出と,Rubyの柔軟性を両立させることを目指す. 本論文では,Gradual typingに基づく動的型と型注釈の構文を加えたRubyのサブセットを考え,そのサブセットについて型付け規則と評価規則を与え,実装に向けての基本的な考え方を示す. さらにその正当性を,進行定理と保存定理を証明することで示す.