型安全な版(バージョン)プログラミング

プログラミング言語の多くは版を言語意味論の外で扱っています。プログラムはある版のモジュールを想定して記述、型検査、コンパイルされた後に、時によっては異なる版と差し替えられて結合・実行されます。そのために衝突や矛盾といった問題をしばしば引き起こしています。

本プロジェクトはプログラミング言語の内部、即ち意味論の中で版を扱うことを提案します。全ての値に(概念的には)版を付ける方法を採り、異なる版のモジュールを同時に使用を可能にしながらも型安全性を保つ理論と実現方式を探ります。

現在は核となる計算系λVL、版付きOOP言語BatakJavaの設計と実現、これらを用いた版付きソフトウェア開発の事例研究について研究を進めています。