研究実績の概要 |
交付申請書で挙げた3つの課題について以下のような成果が得られた. 課題(1)の,動的な言語機構のための漸進的型付けについては,昨年度構築した理論の制限を,Murase と Nishiwaki による多相文脈の研究を元にして緩めることを考え,体系の変更を行った.また,漸進的型付けとML型推論を組み合わせる際の問題点を発見し,実行時型推論と呼ばれる機構で解決できることを示した(POPL2019で発表). 課題(2)の,計算効果をもつ言語のための統一的な漸進的型付けについて,ノミナルゲーム意味論の上での漸進的型付けを研究する計画だったが,その元となる公開契約計算のトレース意味論について証明の細部の修正を行っており進展していない.限定継続については,継続操作を行うことを動的に検査する機構を考案し,その意味論の定義と実装を行った.また,ノミナルゲーム意味論の研究が滞ったため,代替アプローチとして計算効果を一般的に扱う枠組みであるエフェクトハンドラーと多相性とを組み合わせる研究を行い,新しいエフェクトハンドラーのための多相型システムの構築に成功した(ESOP2019で発表).また,昨年度の非決定計算への顕在的契約を導入する理論について成果をまとめ論文発表を行った(PPDP2018で発表). 課題(3)の,漸進的型付けの効率的な実装技術の理論については,漸進的型付けの元で末尾再帰の最適化が行えないという問題を解決する,コアーション渡しによるコンパイル手法の研究を行った(PPL2019で発表). その他,課題(2)に関連して,通信プロトコルを型として記述するセッション型の体系の漸進化の研究についてはより標準的な通信プリミティブのもとでの漸進化の研究を進めた(BEAT2019で発表).
|