研究課題
基盤研究(B)
本研究の目標は、型理論と制約解消技術によるソフトウェアプログラムの正しさの検証である。特に、「依存篩型(dependent refinement types)」と「述語制約(predicate constraint)」を用いた手法の深化を目指す。