研究課題
挑戦的萌芽研究
「難解な専門用語の使用はできるだけ避けるか…適宜説明を加えて」「最大300文字」との指示に従って述べる。「継続」とは、計算機プログラムを実行している途中の「残りの計算」を指す概念である。「文脈」とは、プログラム中のある部分に対し、そのまわりの部分（前者を[]という記号で置き換えた、「穴」のあるプログラム）を指す。本研究では、「継続」を扱う機能の一つであるcall/ccという演算を含む関数型（式の値を計算する「評価」以外の、いわゆる「副作用」がない）プログラムの等価性（動作の等しさ）を証明するための理論を「環境双模倣」という手法にもとづき確立し、その知見を他の研究にも活かすことができた。
現代社会において計算機を中心とする情報処理システムの重要性は言をまたないが、多くの計算機ソフトウェアの理論的基礎は薄弱であり、毎日のように「不具合」（という名の誤動作）を起こして社会的問題となっている。本研究のような「プログラミング言語理論」は、狭義の「プログラム」のみならず、広義の「計算モデル」も含め、数理論理学的基礎による堅固な理論の確立・発展・応用を目指している。本研究もその一つであり、前述の「継続」と「文脈」という、広義の計算機プログラムにおいて重要な概念を扱った、「二つのプログラムの動作が等しい」という基本的な性質を証明する手法の成果である。
すべて 2019 2018 2017 2016
すべて 雑誌論文 (3件) (うち査読あり 3件、 オープンアクセス 2件、 謝辞記載あり 1件) 学会発表 (4件) (うち国際学会 2件)
Lecture Notes in Computer Science
巻: 10818 ページ: 1-16
10.1007/978-3-319-90686-7_1
Functional and Logic Programming: 14th International Symposium, FLOPS 2018
巻: 印刷中
Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, Lecture Notes in Computer Science
巻: 10017 ページ: 171-186
10.1007/978-3-319-47958-3_10
