Derivation of an Abstract Machine for λ-calculus with Delimited-Continuation Constructs
-
- KITANI Arisa
- Ochanomizu University
-
- ASAI Kenichi
- Ochanomizu University
Bibliographic Information
- Other Title
-
- 限定継続処理の抽象機械導出のためのプログラム変換
- PPL2009 ゲンテイ ケイゾク ショリ ノ チュウショウ キカイ ドウシュツ ノ タメ ノ プログラム ヘンカン
Search this article
Abstract
The goal of our research is to give a verified abstract machine for the λ-calculus with delimited continuation constructs, shift and reset, and ultimately to give a formal foundation for the direct implementation of shift/reset in the machine language. Toward this goal, we derive an abstract machine and transition rules from the CPS interpreter defining shift/reset, using a series of transformations whose correctness is already proved. Following the “functional correspondence” approach advocated by Danvy, we first perform the CPS transformation and defunctionalization. Unlike the previous approach, however, we formally introduce two new transformations, stack introduction and environment storing, to turn the interpreter closer to the actual implementation. In this article, we show outline and validity of the two transformations. As a result, we obtain an abstract machine that stores bindings in the stack from the original CPS interpreter using validated transformations only. In the future, after additional transformations, we expect that this abstract machine is turned into a virtual machine, which is similar to the existing machine language implementation.
Journal
-
- Computer Software
-
Computer Software 27 (3), 51-66, 2010
Japan Society for Software Science and Technology
- Tweet
Details 詳細情報について
-
- CRID
- 1390001204738494080
-
- NII Article ID
- 10026562906
-
- NII Book ID
- AN10075819
-
- NDL BIB ID
- 10790835
-
- ISSN
- 02896540
-
- Data Source
-
- JaLC
- NDL
- CiNii Articles
- KAKEN
-
- Abstract License Flag
- Disallowed