階層化コントロールオペレータに対する型システムの構築

• 鈴木, 輝信

• 亀山, 幸義

書誌事項

タイトル別名

• カイソウカ コントロール オペレータ ニ タイスル カタ システム ノ コウチク
• Construction of a Type System for Layered Control Operators

抄録

本論文は，関数型プログラム言語におけるコントロールオペレータを対象とし，これに対する型システムの構築とその性質について述べる．本論文で対象とするshift/reset は，限定継続を操作するコントロールオペレータであり，その意味がCPS 変換に基づいて厳密に定義されているため，形式的に扱いやすいという特徴がある．shift/reset は様々な制御構造を表現できるが，複数の異なる目的でshift/reset を用いると，それぞれのshift/reset が干渉しあい，プログラマの意図どおりにプログラムが実行されない場合がある．そこで，それぞれのshift/reset を区別するため，shift/reset に自然数のレベルを付与して階層化することが提案されている．階層化shift/reset に対して，これまで，型システムやその性質について十分には検討されておらず，ML などの型を持つプログラム言語に階層化shift/reset を直接導入することはできなかった．我々は，先行研究において，レベル2 のshift/reset の型システムを構築したが，この方式では，1 つの項の型付けにおいて，レベルの指数関数の個数の型を必要とするため，レベル3 以上の型システムに拡張することは困難であった．本論文では，任意レベルの階層化shift/reset に対する型システムを提案し，型システムの健全性などの望ましい性質が成立することを示す．これにより，型があるプログラム言語に階層化shift/reset を導入できるようになると考えられる．

We construct a type system for control operators in functional programming languages. Specifically, we treat the layered version of the control operators shift and reset whose semantics is defined in terms of (iterated) CPS translations. While shift and reset are capable of representing various control structures, we cannot have two or more different uses of shift and reset in a single program since they may interfere with each other. In order to avoid this interference, shift and reset should be layered, that is, we should assign to each occurrence of shift and reset a natural number which designates its level. Although it is apparent that a sound type system for layered shift and reset is necessary to introduce them to practical programming languages, no work has ever tried to construct a sufficiently expressive type system for them. In this paper we refine our previous work which solved this problem for the case of level-2, and propose a type system for an arbitrary level. We show that desirable properties such as type soundness hold for this type system, which enables one to introduce the layered shift and reset to statically typed programming languages.

収録刊行物

• 情報処理学会論文誌プログラミング（PRO）

  情報処理学会論文誌プログラミング（PRO） 48 (SIG10(PRO33)), 138-150, 2007-06-15

  東京 : 情報処理学会

キーワード

• 通常論文

詳細情報

• CRID: 1050282812867212160
• NII論文ID: 110006291062
• NII論文ID: 10019381619
• NII書誌ID: AA11464814
• ISSN: 18827802
• ISSN: 03875806
• NDL書誌ID: 8862263
• Web Site: http://id.nii.ac.jp/1001/00016508/
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I8862263
• 本文言語コード: ja
• 資料種別: article
• データソース種別:
  • IRDB
  • NDL
  • CiNii Articles
  • KAKEN