静的型システムと動的型システムの両者の利点を活かす枠組みとして，SiekとTahaは漸進的型付けを提唱している．漸進的型付けでは，型宣言された部分のみ静的型検査が行なわれ，残りの部分については実行時検査が行なわれる．これにより，当初型を付けずに書いたプログラムに型宣言を徐々に付加し，静的型付けされたプログラムを完成させることができる．本研究では，漸進的型付けをクラスに基づくオブジェクト指向言語で実現する理論的基盤として，Igarashi, Pierce, Wadlerらの計算体系Featherweight Java (FJ)に動的型を導入した体系FJ^?を定義し，型付け規則を与える．さらにFJ^?からFJにリフレクションを加えた体系への変換を定義することで意味論を与え，静的に検査した部分の安全性が保証されることを示す．