New reational program semantics based on the notion of continuations and contexts

2018 Fiscal Year Final Research Report

• Project/Area Number: 16K12409
• Research Category: Grant-in-Aid for Challenging Exploratory Research
• Allocation Type: Multi-year Fund
• Research Field: Software
• Research Institution: Tohoku University
• Principal Investigator: Sumii Eijiro 東北大学, 情報科学研究科, 教授 (00333550)
• Research Collaborator: Matsuda Kazutaka ; Kiselyov Oleg
• Project Period (FY): 2016-04-01 – 2019-03-31
• Keywords: 継続 / （評価）文脈 / プログラム等価性 / call/cc / λ計算 / （環境）双模倣

Outline of Final Research Achievements

A theory for proving program equivalence, based on environmental bisimulations, has been developed in a foundational calculus modelling a functional programming language with the undelimited continuation operator "call/cc" (call-with-current-continuation).

Free Research Field

プログラム理論

Academic Significance and Societal Importance of the Research Achievements

現代社会において計算機を中心とする情報処理システムの重要性は言をまたないが、多くの計算機ソフトウェアの理論的基礎は薄弱であり、毎日のように「不具合」（という名の誤動作）を起こして社会的問題となっている。本研究のような「プログラミング言語理論」は、狭義の「プログラム」のみならず、広義の「計算モデル」も含め、数理論理学的基礎による堅固な理論の確立・発展・応用を目指している。本研究もその一つであり、前述の「継続」と「文脈」という、広義の計算機プログラムにおいて重要な概念を扱った、「二つのプログラムの動作が等しい」という基本的な性質を証明する手法の成果である。