4 種類の限定継続演算子のための型システム
石尾 千晶, 浅井 健一
お茶の水女子大学
ishio.chiaki@is.ocha.ac.jp, asai@is.ocha.ac.jp
概 要
限定継続演算子には多くの種類があり、それぞれ異なる特徴を持つ。中でも
control0/prompt0 は、切り取った継続を呼び出す文脈や、現在の限定継続のひとつ
外側の継続を操作できることが知られている。control0 を使うと、継続を切り取ることができる範囲が動的になる式を書けることから、shift のような演算子に比べて型システムが複雑になる。これまで、shift/reset, control/prompt, shift0/reset0などの型システムを、CPS インタプリタから導出する研究がなされていたが、本研究ではこの方法を control0/prompt0 にも適用し型システムを導出する。この方法を拡張して、shift, control, shift0, control0 の 4 種類の演算子を含む λ 計算に対する一般的な型システムを導出し、定理証明系言語 Agda で実装する。また、既存研究の型システムとの関係を明らかにする。

1

はじめに

限定継続演算子とは、限定された範囲の継続を操作することができる演算子のことで、継続を捕捉する演算子と、継続の範囲を限定する演算子を組み合わせて継続を操作する。中でも、代表的な演算子である shift (Sk. e) [9], control (Fk. e) [10], shift0 (S0 k. e) [7], control0 (F0 k. e) [12]は、いずれも直近の限定子まで継続を切り取る演算子だが、これらは次のような動作の違いがある。

⟨(Sk. e) + 3⟩ = ⟨e[λx. ⟨x + 3⟩/k]⟩⟨(S0 k. e) + 3⟩ = ⟨e[λx. ⟨x + 3⟩/k]⟩⟨(Fk. e) + 3⟩ = ⟨e[λx. ⟨x + 3⟩/k]⟩⟨(F0 k. e) + 3⟩ = ⟨e[λx. ⟨x + 3⟩/k]⟩

各演算子を shift と比較してみると、control は、切り取った継続 k の body 部分に限定子 ⟨ ⟩がつかず、shift0 は、継続を切り取った後、e の周りに限定子が残らない。また control0 では
その両方が起きている。
例えば ⟨⟨(S0 k1 . S0 k2 . e) + 1⟩ + 2⟩ のように shift0 がネストしている例を考えてみる。まず
S0 k1 . . . . が実行されると、k1 = λx. ⟨x + 1⟩ となって、直近の限定子までの継続を切り取るが、次に S0 k2 . . . . が実行されると、直近の限定子よりもさらにひとつ外側の限定子に囲まれた継続まで
アクセスできるようになるため、k2 = λx. ⟨x + 2⟩ となる。この「直近の限定子よりも外側にある継続」を以下では「メタ継続」と呼ぶ。shift0 のようにメタ継続にアクセスできる演算子では、捕捉できる限定継続の範囲が動的に変化するため、型システムを考えるにはメタ継続を追跡する必要がある。
一方 control はどうだろうか。以下の式を例にとって考えてみる。

⟨⟨(λx. Fk2 . x) (Fk1 . (2 + k1 1))⟩⟩= ⟨⟨2 + k1 1 [λy. (λx. Fk2 . x) y/k1 ]⟩⟩= ⟨⟨2 + Fk2 . 1⟩⟩= ⟨⟨1 [λx. 2 + x/k2 ]⟩⟩1この例では、最初に切り取った継続 k1 の中に、さらに control が入っている。control では切り取った継続の body 部分に限定子がつかないので、k1 の中の control がどこまで継続を切り取るのかは、k1 が呼び出されるまでわからない。実際に k1 を呼び出すと、呼び出された文脈におけ
る直近の限定子まで継続を切り取るので、今回の例では k2 = λx. 2 + x となっている。control
を含む式の型付けをおこなうには「切り取った継続が呼び出される文脈」を追跡する必要があり、以下ではこれを「呼び出し文脈」と言うものとする。1 また、control0 では、呼び出し文脈だけでなく、メタ継続も追跡する必要がある。
このように、control, shift0, control0 では、継続が切り取ることのできる範囲が動的に変化するため、shift に比べると型システムは複雑になる。これまで、型なしの状況下でこれらの限定継続演算子どうしの関係性が明らかにされてきた [14, 18] が、型付きの状況下では、shift や
shift0 などの CPS の階層の関係の研究 [16] などがあるものの、異なる限定継続演算子同士の関係性はまだ明らかになっていない。
本研究では、限定継続演算子の中でも代表的な shift/reset, control/prompt, shift0/reset0,
control0/prompt0 の 4 種類を取り上げる。これまでにまだ一般的な型システムが導出されていなかった control0/prompt0 の型規則を導出し、control0/prompt0 も含めた 4 種類の演算子のための統一的な型システムを構築する。本研究の型システムは、定理証明系言語 Agda [17] で実装されており、そのソースコードは https://github.com/chiaki-i/type4d で入手可能である。
本論文の構成は次の通りである。2 節で構文と CPS インタプリタを定義し、3 節でその型シス
テムを導出する。4 節で先行研究の型システムとの比較をおこない、5 節では Agda による実装について触れる。また、6 節で関連研究を紹介して、最後に 7 節でまとめと今後の展望を述べる。
本論文での表記について 本論文では、数式中で色を使うため、カラーで印刷すると読みやすい。
(波線) で示す。ま
呼び出し文脈にかかわる箇所を赤字 (下線)で、メタ継続にかかわる箇所を青字::::::::::
τた、e のように項の右肩に赤字で型を表すことがある。

構文と CPS インタプリタ

2

本節では、この論文で扱う言語 λD と λC を定義し、λD から λC に継続渡し形式 (continuationpassing style; CPS) に変換するインタプリタ (以下、CPS インタプリタ) も定義する。λD は、
CPS インタプリタの入力言語で、限定継続演算子を含む λ 計算である。一方 λC は CPS インタ
プリタの出力言語で、継続渡し形式で書かれている。

2.1

λD の構文図 1 に、λD の構文を示す。λD は、値呼びの単純型付き λ 計算に、4 種類の限定継続演算子を加えたものとなっている。項 e には、値と関数適用のほかに、継続を切り取る演算子として shift,control, shift0, control0 と、限定子を加えた。この限定子は、継続を切り取る演算子に対応
して reset, prompt, reset0, prompt0 のように異なる名前で呼ばれることがあるが、中身はどれも同じふるまいをするものである [14] ため統一して表記する。

1

この「呼び出し文脈」は英語では “a trail of invocation contexts” に相当するため、他の文献では「トレイル」と呼ぶことがある。

2

値 v
項

:= n | x | λx. ee := v | e1 e2 | Sk. e | F k. e | S0 k. e | F0 k. e | ⟨e⟩

項の型 τ:= N | τ1 → τ2 ⟨µα , σα ⟩ α ⟨µβ , σβ ⟩ β

呼び出し文脈の型 µ := •µ | τ1 → ⟨µ, σ⟩ τ2
メタ継続の型 σ := •σ | ((τ1 → ⟨µ1 , σ1 ⟩ τ2 ) × µ2 ) :: σ2
図 1. λD の構文

項の型 τ は、自然数型と、矢印型からなる。矢印型 τ1 → τ2 ⟨µα , σα ⟩ α ⟨µβ , σβ ⟩ β は、
「τ1 → τ2型の関数を、『µα 型の呼び出し文脈と σα 型のメタ継続のもとで実行した結果が α 型になるような継続』と、µβ 型の呼び出し文脈、σβ 型のメタ継続を渡して実行すると、その結果は β 型になる」ことをあらわしている。関数の body 部分に限定継続演算子が含まれていると、α と β が異なる型になる可能性がある。
ここで、「ある継続のもとで実行した結果の型」、つまり限定継続が返す型のことを、answer
type [1] と呼ぶ。図 1 に定義されている矢印型では、α 型と β 型がそれにあたる。α 型は、項の実行前に、項全体が返すと予想される型 (initial answer type) をあらわし、β 型は、実際に式を実行したときに、最終的に項が返す型 (ﬁnal answer type) をあらわす。例えば、isZero が (int-> bool) 型の関数だとすると、⟨(λx. isZero (x − 1)) 1⟩ のような式では、関数部分 (λx. . . .) のinitial answer type と ﬁnal answer type の両方とも bool 型となる。一方で、関数の body 部分に
shift が入った ⟨(λx. isZero (Sk. x − 1)) 1⟩ のような式では、関数部分 (λx. . . .) の initial answer
type は bool 型、ﬁnal answer type は int 型となり、answer type が変化する。
呼び出し文脈やメタ継続については、限定継続演算子の実行時に内部で操作がおこなわれるものなので、2.2, 2.3 節のように CPS になるまで明確な項はあらわれない。呼び出し文脈の型 µ は、
空 •µ であるか、「τ1 型の値、µ 型の呼び出し文脈、σ 型のメタ継続を受け取ると、τ2 型の値を返す」継続であるかのいずれかである。メタ継続は、空 •σ であるか、継続と呼び出し文脈のペアが入れ子状にメタ継続に積まれているかのどちらかである。

2.2

λC の構文

この節では、CPS インタプリタの出力言語である λC を定義する。λC は、値呼びの単純型付
き λ 計算に、unit 型と直積型を加えた体系で、構文は図 2 の通りとなる。
継続を λC で書くと λv. λt. λm. . . . のように表され、値 v 、呼び出し文脈 t、メタ継続 m を受け取ると計算結果を返す関数である。呼び出し文脈の実装方法には、関数やリストなど複数あるが、今回は Shan [18] に従って関数 λv. λt. λm. . . . として扱う2 。また、メタ継続は ((k, t), m)のように、そのときの継続 k と呼び出し文脈 t のペアを、入れ子にして表現する。呼び出し文脈やメタ継続が空の場合は、いずれも unit 型の値 () とする。

呼び出し文脈の中に、(int → µ1 → σ1 → int), (string → µ2 → σ2 → int), . . . のように、異なる型を持つ複数の継続が現れる場合に対応するためには、heterogeneous list もしくは関数を使って実装すればよい。詳しくは [6]を参照されたい。
2

3

値 v

:= n | () | x | λx. e

項 e := v | e1 e2 | (e1 , e2 )型 τ:= int | unit | τ1 → τ2 | τ1 × τ2
図 2. λC の構文

N∗ = int(τ1 → τ2 ⟨µα , σα ⟩ α ⟨µβ , σβ ⟩ β)∗ = τ1∗ → (τ2∗ → µ∗α → σα∗ → α∗ ) → µ∗β → σβ∗ → β ∗•∗µ = unit
(τ1 → ⟨µ, σ⟩ τ2 )∗ = τ1∗ → µ∗ → σ ∗ → τ2 ∗•∗σ = unit(((τ1 → ⟨µ1 , σ1 ⟩ τ2 ) × µ2 ) :: σ2 )∗ = ((τ1∗ → µ∗1 → σ1∗ → τ2 ∗ ) × µ2 ∗ ) × σ2 ∗図 3. λD の型の CPS 変換

2.3

λD から λC への CPS インタプリタ

この節では、λD から λC への型レベルの CPS 変換と、項の CPS インタプリタを定義する。
図 3 では、型レベルの CPS 変換 ∗ を定義している。λD で継続の型は (τ1 → ⟨µ1 , σ1 ⟩ τ2 ) と書いたが、これを CPS にすると、値・呼び出し文脈・メタ継続を順番に引数として受け取って値を返す関数になっている。
次に、図 4 では、E[[e]] は、実行時に環境 ρ 、継続 κ、呼び出し文脈 t、メタ継続 m を受け取って処理をおこなう。このインタプリタ規則は、2CPS 3 のインタプリタ [7] に、呼び出し文脈に相当する引数 t を加えたものであり、Shan による 4 種類の限定継続演算子のための型なし CPS イ
ンタプリタ [18] を η-展開したものに等しい。図 4 では、呼び出し文脈にかかわる箇所を赤字 (下線) で、メタ継続にかかわる箇所を青字 (波線) で示している。
限定継続演算子の規則では、いずれも、切り取ってきた継続を λv. λκ′ . λt′ . λm′ . . . . のように書き起こして、それを k に束縛した上で、再帰的に e の実行を進めている。
shift や control では、継続を切り取った後も、限定継続演算子を囲んでいた直近の限定子が残るので、初期継続 kid と空の呼び出し文脈 () 、そしてメタ継続は変わらず m のままで e が実行される。初期継続 kid は、図 4 に定義が示されている通り、値・呼び出し文脈・メタ継続を受け取って、呼び出し文脈に積まれた継続を実行し、その後呼び出し文脈が空になったら、メタ継続に積まれた継続を順に実行する関数である。一方、shift0 や control0 では、限定継続演算子
が継続を切り取ると、直近の限定子がなくなって、メタ継続にアクセスできるようになる。そのため、引数として受け取るメタ継続の形は ((κ0 , t0 ), m0 ) のように展開されて中身が使えるような形で書かれている。e を再帰的に実行するときには、そのときの継続 κ0 と呼び出し文脈 t0 、eの実行時のメタ継続 m0 が渡される。
では、切り取られる継続 k の中身は、各演算子ごとにどのような形をとるだろうか。shift や
3

CPS で書かれた式をさらに CPS 変換にかけたもののことを 2CPS と呼ぶ。一般的な CPS では、そのときの継続を受け取って計算を進めるのに対して、2CPS は、そのときの「継続の継続」(メタ継続) と、そのときの継続、という両方を受け取って計算を進めていく。また、2CPS と区別するために、普通の CPS のことを 1CPS と呼ぶことがある。

4

kid v () () = v
kid v () ((k0 , t0 ), m0 ) = k0 v t0 m0
kid v t m = t v () m() @ t = t
k @ t = k :: tE[[x]] ρ κE[[n]] ρ κE[[λx. e]] ρ κE[[e1 e2 ]] ρ κ
E[[Sk. e]] ρ κ

=
=
=
=
=

k :: () = k
k :: t = λv. λt′ . λm′ . k v (t :: t′ ) m′

λt. λm. κ ρ(x) t m
λt. λm. κ n t m
λt. λm. κ (λv. E[[e]] ρ[v/x]) t m
λt. λm. E[[e1 ]] ρ (λv1 . λt1 . λm1 . E[[e2 ]] ρ (λv2 . λt2 . λm2 . v1 v2 κ t2 m2 ) t1 m1 ) t m
λt. λm. E[[e]] ρ[λv. λκ′ . λt′ . λm′ . κ v t ((κ′ , t′ ), m′ )/k] kid () m:::::::::::

λt. λm. E[[e]] ρ[λv. λκ′ . λt′ . λm′ . κ v (t @ (κ′ :: t′ )) m′ /k] k

E[[Fk. e]] ρ κ =id () m′ ′′′′E[[S0 k. e]] ρ κ = λt. λ((κ0 , t0 ), m0 ). E[[e]] ρ[λv. λκ . λt . λm . κ v t ((κ , t ), m′ )/k] κ0 t0 m0::::::::::::::::::::::::::::::

E[[F0 k. e]] ρ κ = λt. λ((κ0 , t0 ), m0 ). E[[e]] ρ[λv. λκ′ . λt′ . λm′ . κ v (t @ (κ′ :: t′ )) m′ /k] κ0 t0 m0:::::::::::::::::::

E[[⟨e⟩]] ρ κ = λt. λm. E[[e]] ρ kid () ((κ, t) , m)
図 4. λD の CPS インタプリタ

shift0 では、k の呼び出し時の継続 κ′ や呼び出し文脈 t′ は、((κ′ , t′ ), m′ ) のように、現在のメタ継続とペアにする形で追加されていく。一方、control や control0 のように呼び出し文脈が動的に定まる演算子では、κ′ や t′ は (t @ (κ′ :: t′ )) という形で呼び出し文脈に追加されている。ここで使われている演算子 @ は呼び出し文脈どうしを結合し、 :: は継続を呼び出し文脈に追加している。本研究では、呼び出し文脈も継続と同様に、関数であらわされるので、 @ も :: も内部的には関数合成をしている。4
最後に、⟨e⟩ では、限定子の内側の項 e を再帰的に実行している。⟨e⟩ の外側の継続は、e にとってのメタ継続に相当するので、現在の継続 κ と呼び出し文脈 t をメタ継続に積んだ上で計算を進めている。
このインタプリタは、3 節で述べる型規則のもとで、定理証明系言語 Agda で実装されている。
そのため、CPS インタプリタが型を保存することや、λD の項に型がつけば CPS インタプリタが止まることが示せている。

型システムの導出

3λD の型システムを図 5 に示す。型判断は Γ ⊢ e : τ ⟨µα , σα ⟩ α ⟨µβ , σβ ⟩ β と書いて、「型環境 Γのもとで項 e は τ 型を持つ。『µα 型の呼び出し文脈と σα 型のメタ継続のもとで、answer typeが α 型になるような継続』と、µβ 型の呼び出し文脈、σβ 型のメタ継続のもとで e を実行すると、
answer type は β 型になる。」と読む。
本研究において、control0/prompt0 の型規則が新たに導出した規則である。特に、限定子のための型規則は、reset, prompt, reset0, prompt0 を包含する一般的な規則となっている。また、
4@ や :: は、Shan の論文 [18] における compose 関数に等しい。もし、呼び出し文脈を heterogeneous list で実装する場合は、それぞれリスト用の append や cons を用いて実装すればよい。

5Γ ⊢ e : τ ⟨µα , σα ⟩ α ⟨µβ , σβ ⟩ β
x : τ ∈Γ
(TVar)Γ ⊢ x : τ ⟨µα , σα ⟩ α ⟨µα , σα ⟩ αΓ ⊢ n : N ⟨µα , σα ⟩ α ⟨µα , σα ⟩ α(TNum)

Γ, x : τ1 ⊢ e : τ2 ⟨µα , σα ⟩ α ⟨µβ , σβ ⟩ β(TLam)Γ ⊢ (λ x. e) : (τ1 → τ2 ⟨µα , σα ⟩ α ⟨µβ , σβ ⟩ β) ⟨µγ , σγ ⟩ γ ⟨µγ , σγ ⟩ γ
Γ ⊢ e1 : (τ1 → τ2 ⟨µα , σα ⟩ α ⟨µβ , σβ ⟩ β) ⟨µγ , σγ ⟩ γ ⟨µδ , σδ ⟩ δΓ ⊢ e2 : τ1 ⟨µβ , σβ ⟩ β ⟨µγ , σγ ⟩ γΓ ⊢ (e1 e2 ) : τ2 ⟨µα , σα ⟩ α ⟨µδ , σδ ⟩ δ(TApp)

id-cont-type(γ, µid , σid , γ ′ )Γ, k : τ → τ1 ⟨µ1 , σ1 ⟩ τ2 ⟨µ2 , σ2 ⟩ α ⊢ e : γ ⟨µid , σid ⟩ γ ′ ⟨•µ , σβ ⟩ βΓ ⊢ Sk. e : τ ⟨µβ , (((τ1 → ⟨µ1 , σ1 ⟩ τ2 ) × µ2 ) :: σ2 )⟩ α ⟨µβ , σβ ⟩ βid-cont-type(γ, µid , σid , γ ′ )compatible((τ1 → ⟨µ1 , σ1 ⟩ τ2 ), µ2 , µγ ) compatible(µβ , µγ , µα )Γ, k : τ → τ1 ⟨µ1 , σ1 ⟩ τ2 ⟨µ2 , σα ⟩ α ⊢ e : γ ⟨µid , σid ⟩ γ ′ ⟨•µ , σβ ⟩ βΓ ⊢ Fk. e : τ ⟨µα , σα ⟩ α ⟨µβ , σβ ⟩ βΓ, k : τ → τ1 ⟨µ1 , σ1 ⟩ τ2 ⟨µ2 , σ2 ⟩ α ⊢ e : τ0 ⟨µ0 , σ0 ⟩ τ0′ ⟨µ′0 , σ0′ ⟩ β(TShift)(TControl)(TShift0)

Γ ⊢ S0 k. e : τ ⟨µβ , (((τ1 → ⟨µ1 , σ1 ⟩ τ2 ) × µ2 ) :: σ2 )⟩ α ⟨µβ , (((τ0 → ⟨µ0 , σ0 ⟩ τ0′ ) × µ′0 ) :: σ0′ )⟩ βcompatible((τ1 → ⟨µ1 , σ1 ⟩ τ2 ), µ2 , µγ ) compatible(µβ , µγ , µα )Γ, k : τ → τ1 ⟨µ1 , σ1 ⟩ τ2 ⟨µ2 , σα ⟩ α ⊢ e : τ0 ⟨µ0 , σ0 ⟩ τ0′ ⟨µ′0 , σ0′ ⟩ β(TControl0)Γ ⊢ F0 k. e : τ ⟨µα , σα ⟩ α ⟨µβ , (((τ0 → ⟨µ0 , σ0 ⟩ τ0′ ) × µ′0 ) :: σ0′ )⟩ β
id-cont-type(γ, µid , σid , γ ′ )Γ ⊢ e : γ ⟨µid , σid ⟩ γ ′ ⟨•µ , (((τ → ⟨µα , σα ⟩ α) × µβ ) :: σβ )⟩ β
Γ ⊢ ⟨e⟩ : τ ⟨µα , σα ⟩ α ⟨µβ , σβ ⟩ β(TPrompt0)

id-cont-type(τ, •µ , •σ , τ ′ ) = τ ≡ τ ′id-cont-type(τ, •µ ,= (τ ≡ τ1 ) ∧ (τ ′ ≡ τ1′ ) ∧ (µ1 ≡ µ2 ) ∧ (σ1 ≡ σ2 )(((τ1 → ⟨µ1 , σ1 ⟩ τ1′ ) × µ2 ) :: σ2 ), τ ′ )id-cont-type(τ, (τ1 → ⟨µ1 , σ1 ⟩ τ1′ ), σ2 , τ ′ ) = (τ ≡ τ1 ) ∧ (τ ′ ≡ τ1′ ) ∧ (µ1 ≡ •µ ) ∧ (σ1 ≡ σ2 )compatible(•µ , µ2 , µ3 )compatible((τ1 → ⟨µ1 , σ1 ⟩ τ1′ ), •µ , µ3 )compatible((τ1 → ⟨µ1 , σ1 ⟩ τ1′ ),(τ2 → ⟨µ2 , σ2 ⟩ τ2′ ), •µ )compatible((τ1 → ⟨µ1 , σ1 ⟩ τ1′ ),(τ2 → ⟨µ2 , σ2 ⟩ τ2′ ), (τ3 → ⟨µ3 , σ3 ⟩ τ3′ ))= µ2 ≡ µ3= (τ1 → ⟨µ1 , σ1 ⟩ τ1′ ) ≡ µ3
= ⊥= (τ1 ≡ τ3 ) ∧ (τ1′ ≡ τ3′ ) ∧ (σ1 ≡ σ3 )∧(compatible((τ2 → ⟨µ2 , σ2 ⟩ τ2′ ), µ3 , µ1 ))図 5. λD の型システム

6

そのほかの shift, control, shift0 のための型規則も、CPS インタプリタで呼び出し文脈やメタ継続に対する操作をおこなうのにあわせて拡張している。

3.1

control0 の型規則の導出

図 5 の型規則はすべて図 4 から導出されているため、型規則の中身をひとつひとつ CPS イン
タプリタと対応付けるとわかりやすい。そこで、(TControl0) を例にとって導出過程を追ってみることにする。以下に、control0 のインタプリタの各項に対して型を割り当てる順番を示した
ものと、型を割り当て終えたものを示す。
234E[[F k. e]] ρ κ = λt 1 . λ((κ , t ), m ). E[[e]] ρ[λv 7 . λκ′ 7 . λt′ 7 . λm′ 7 .
0

0

0

0

(κ 9 v 8 (t 5 @ (κ′ 8 :: t′ 8 ) 11 ) 12 m′ 8 ) 10 / k]µ∗β(τ0 → ⟨µ0 , σ0 ⟩ τ0′ )∗

µ′0

∗

σ0′

E[[F0 k. e]] ρ κ = λt . λ((κ0, t0 ), m0
∗
∗
∗
∗
τ
′
(τ
→
⟨µ
,
σ
⟩
τ
)
′
µ
1
1
1
2
2
E[[e]] ρ[λv . λκ
. λt . λm′σ2 .

κ0

6

t0

6

m0

6

∗

).

∗
∗
∗
∗
∗ µ∗
∗
∗ ∗
∗
∗
∗
(κ(τ → µα → σα → α ) v τ (t β @ (κ′(τ1 → ⟨µ1 , σ1 ⟩ τ2 ) :: t′µ2 )µγ )µα m′σα )α / k]∗∗(τ → ⟨µ0 , σ0 ⟩ τ0′ )∗ µ′0
σ′t0 m0 0κ0 0型規則を導出するには、まず λ 抽象で新たに導入された変数に対して新しい型変数名を割り当て、その後、関数適用などの条件を加味して型を決めていくという方法をとる。
control0 のインタプリタ規則の冒頭で、呼び出し文脈 t と、メタ継続 ((κ0 , t0 ), m0 ) が λ 抽象で導入されている。control0 はメタ継続の中身にアクセスできることから、初めからメタ継続は展開された形で表記されている。これらの変数のうち、t, t0 , m0 については新しい型変数をおく ( 1 〜 4 )。その中でも、κ0 は継続であるため、型は (? → ⟨?, ?⟩ ?)∗ の形をとるはずで、それに応じて型変数をおく ( 2 )。この導出過程全体を通して注意したいのが、CPS インタプリタの各
項に型をつけるという作業をしているので、これまで定めた型も、正確には、型レベルの CPS 変
換 (図 3) がかかっているという点である。そのため型変数の右肩に CPS 変換を示す ∗ がついていることがわかる。例えば κ0 の型も、CPS 変換されると次のように展開できる。これ以降の説
明では、変換前後の 2 つの表記を区別せずに扱う。
∗(τ0 → ⟨µ0 , σ0 ⟩ τ0′ )∗ = (τ0∗ → µ∗0 → σ0∗ → τ0′ )同じ変数には同じ型が割り振られるので、インタプリタ内に現れる t, κ0 , t0 , m0 の型も定まる( 5 , 6 )。control0 の body 部分である e に対して再帰的に CPS インタプリタを実行する際、切り取った継続は k に束縛され、それが環境 ρ に登録される。切り取った継続 k の中身にも λ抽象が登場するので、上述と同様の方法で型変数をおき ( 7 )、同じ変数名のところにも書き写す( 8 )。ここまで、λ 抽象で導入された変数に対しては、全て新たに異なる型変数をおいている。
次に、インタプリタの実行時に与えられた継続 κ の型について考える。κ は、値 v 、呼び出し
文脈 (t @ κ′ :: t′ )、メタ継続 m′ を受け取る継続であるため、κ の型は、これまでに 8 の手順で定めた v, m′ の型を用いると (τ ∗ → ?∗ → σα∗ → ?∗ ) という形をとるとわかる ( 9 )。継続 κ が返す型については、新たに α∗ とおく ( 10 )。また、呼び出し文脈 (t @ (κ′ :: t′ )) については、全体の型を一旦 µ∗α とし ( 12 )、内側の (κ′ :: t′ ) の型を µ∗γ とする ( 11 )。ここまでで得られた型変数
名を型規則の形に書き直すと、(TControl0) になる。ただし、呼び出し文脈については、3 つの呼び出し文脈 t, κ′ , t′ の型についての制約を、別途示す必要がある。これについては 3.2 節で述
べる。

7

3.2

呼び出し文脈の合成

今回は、呼び出し文脈どうしの合成 @ や継続の追加 :: は、2.3 節で述べた通り、いずれも関数合成で実装されている。そのため図 4 の定義に従って型の制約をくくり出すことにする。呼び出し文脈の型の制約は compatible(µ1 , µ2 , µ3 ) と書くと、(µ1 型の t1 ) @ (µ2 型の t2 ) = (µ3 型の t3 )もしくは (µ1 型の k1 ) :: (µ2 型の t2 ) = (µ3 型の t3 ) に対応している。具体的には、compatible の
1 つ目の規則は () @ t = t に、2 つ目の規則は k :: () = k に対応している。3 つ目の規則は、空でない継続や呼び出し文脈を合成したときの結果は、空の呼び出し文脈にはなりえないことを意味する。4 つ目の規則は一見難しいようだが、k :: t = . . . の式と、次のように対応している。
′ ∗′ ∗k (τ1 → ⟨µ1 , σ1 ⟩ τ1 ) :: t(τ2 → ⟨µ2 , σ2 ⟩ τ2 )
∗
∗
∗
∗ ′∗
∗
∗
∗
∗
′∗
∗
′ ∗
= λv τ3 . λt′ µ3 . λm′ σ3 . (k (τ1 → µ1 → σ1 → τ1 ) v τ3 (t(τ2 → ⟨µ2 , σ2 ⟩ τ2 ) :: t′ µ3 ) m′ σ3 )τ3

式の 2 行目において、継続 k が、値 v を受け取るためには τ1∗ ≡ τ3∗ になればよい。また、k が呼び出し文脈 (t :: t′ ) を受け取るためには、compatible を再帰的に適用させて、(τ2 → ⟨µ2 , σ2 ⟩ τ2′ )∗型と µ∗3 型を持つ呼び出し文脈を合成した結果が、µ∗1 型の呼び出し文脈に一致すればよい。k が受け取るメタ継続や、k が返す型についても同様に対応付けすることで、compatible を導出できる。

3.3

初期継続の型の性質

図 4 の CPS インタプリタでは、shift, control, prompt0 において初期継続を使う場面がある。
これに対応する形で、図 5 の型システムでも、初期継続のための型の制約 id-cont-type が設けられている。(γ → ⟨µid , σid ⟩ γ ′ ) 型を持つ継続が初期継続であるためには、id-cont-type(γ, µid , σid , γ ′ )を満たせばよい。
id-cont-type も、これまでの規則の導出と同様の方法で、対応する kid の定義から素直に導出できる。例えば、id-cont-type の 2 つ目の規則では、kid の規則と以下のように対応づけられる。
∗

∗
′
∗ ′
(kid v τ ()•µ ((k0 , t0 ), m0 )(((τ1 → ⟨µ1 , σ1 ⟩ τ1 ) × µ2 ) :: σ2 ) )τ∗(τ ∗ → µ∗1 → σ1∗ → τ1′ ) τ ∗ µ∗2 σ2∗= k0 1
v t0 m0∗

式の 2 行目で、k0 が引数 v, t0 , m0 を受け取るためには型が一致する必要がある。また、初期継続 kid はもともと τ ′ ∗ 型を返すことになっていたが、それはメタ継続に記録されていた継続 k0 の返す型と一致するはずなので、τ ′ ∗ ≡ τ1′ ∗ となることがわかる。

4

他の型システムとの比較

この節では、本論文で導出した、4 種類の限定継続演算子のための型システム (以下、4D と表記する) と、先行研究で提案されている各限定継続演算子のための型システムを比較する。

4.1

shift/reset

3 節では、Danvy と Filinski による shift/reset の型システム導出の方法 [7] に倣って、CPS
インタプリタから型システムを導出をおこなった。ここでは、その型システムと、4D を比較する。
以下の式は、Danvy と Filinski の型システム (以下、DF と表記する) の shift の型付け規則を、

8

4D の表記に寄せて書いたもの (DF-Shift) である。型判断は Γ ⊢ e : τ, α, β と書いて「項 e は型
環境 Γ のもとで τ 型を持つ。τ → α 型の継続のもとで実行すると最終的に β 型になる」と読む。
Γ, k : τ → α, δ, δ ⊢ e : ϵ, ϵ, β
Γ ⊢ Sk. e : τ, α, β(DF-Shift)

この (DF-Shift) は 1CPS で書かれたインタプリタ [8] をもとに導出されており、呼び出し文脈やメタ継続に相当する引数は含まれないため上のように表記されている。
この型規則を図 5 の (TShift) と比較した時、異なる点は 2 つある。1 つが、shift の body 部
分 e の answer type、もう 1 つが、切り取った継続 k の型判断である。
まず、(DF-Shift) の e の型判断を見てみよう。(DF-Shift) では answer type はいずれも ϵだが、(TShift) では γ, γ ′ となっている。図 5 中の id-cont-type の定義を見ると、必ず γ ≡ γ ′となるのは、呼び出し文脈とメタ継続の両方とも空の場合 (id-cont-type の 1 つ目の規則) のみである。e に限定継続演算子のうちいずれかが現れると、呼び出し文脈やメタ継続に継続が積まれるため γ, γ ′ は異なるものになる可能性がある。
一方、切り取った継続 k の型はどうだろうか。(DF-Shift) では k の矢印型の α が Sk. e のinitial answer type になるが、(TShift) では k は、メタ継続のもとで実行して得られる ﬁnal
answer type である α が Sk. e の initial answer type になる。このような違いが生じたのは、(DF-Shift) の元となるインタプリタが 1CPS で書かれていたのに対して、(TShift) では 2CPSのインタプリタで書かれているからである。shift のための 2CPS インタプリタに基づいて型システムを導出すると、(TShift) から呼び出し文脈を除いたものに等しくなる。

4.2

control/prompt

これまでに、著者らが構築した control/prompt のための型システム [6] は、本論文と同様に、
4.1 節で取り上げた DF の導出方法に則って作られている。control のための型規則は、4D の(TControl) のメタ継続部分を除いたものに一致する。prompt のための型規則を比較するため、以下に [6] から抜粋したものを (TPrompt′ ) として示す。4D の (TPrompt0) とは、型規則の結論部の ⟨e⟩ の型判断が異なる。

id-cont-type(γ, µid , γ ′ ) Γ ⊢ e : γ ⟨µid ⟩ γ ′ ⟨•µ ⟩ τΓ ⊢ ⟨e⟩ : τ ⟨µα ⟩ α ⟨µα ⟩ α(TPrompt′ )これも、4.1 節と同様の理由だが、元となるインタプリタの prompt のみが 1CPS で書かれている
ためこのような違いが現れている。

4.3

shift0/reset0

ここでは、shift0/reset0 の型システムの先行研究として、Materzok と Biernacki による型システム [15] (以下、MB と表記する) と比較する。まずは、比較対象となる構文 λS0 (図 6) と型
システム (図 7) について説明する。

4.3.1

λS0 の構文

λS0 は、値呼びの単純型付き λ 計算に shift0/reset0 を加えたものである。その型は自然数
型 N か、矢印型からなる。また、型注釈は、限定継続演算子によって継続が直接操作される可能性がない (pure である) ことを示す ϵ か、そうでない (impure である) かのいずれかである。
型や型注釈は、単体ではわかりにくいが、型判断の中で一緒に考えると理解しやすい。型判断は
9σ型 τ := N | τ −→ τ′型注釈 σ := ϵ | [τ σ] τ ′ σ ′値 v := n | x | λx. e
項 e := v | e1 e2 | S0 k. e | ⟨e⟩

図 6. λS0 の構文

Γ, x : τx ⊢ x : τx [τ σ] τ σ(MB-Var)Γ, x : τ1 ⊢ e : τ2 σσΓ ⊢ λx. e : τ1 −→ τ2 [τ σ ′ ] τ σ ′(MB-Abs)[τ ′ σ1 ] τ ′ σ3Γ ⊢ e1 : τ1 −−1−−−−3−→ τ2 [τ4′ σ4 ] τ2′ σ2 Γ ⊢ e2 : τ1 [τ3′ σ3 ] τ4′ σ4(MB-App)Γ ⊢ e1 e2 : τ2 [τ1′ σ1 ] τ2′ σ2σ

1Γ, k : τ1 −→τ2 ⊢ e : τ3 σ 2(MB-Shift0)Γ ⊢ S0 k. e : τ1 [τ2 σ1 ] τ3 σ2Γ ⊢ e : τ ′ [τ ′ [τ ′′ σ ′′ ] τ ′′ σ ′′ ] τ σ(MB-Reset0)Γ ⊢ ⟨e⟩ : τ σΓ, x : τ1 ⊢ e : τ2 [τ3 σ3 ] τ4 σ4[τ3 σ3 ] τ4 σ4Γ ⊢ λx. e : τ1 −−−−−−−→ τ2 [τ σ ′ ] τ σ ′(MB-Abs-Ext)[τ4 σ4 ] τ5 σ5Γ, k : τ1 −−−−−−−→ τ2 ⊢ e : τ3 [τ6 σ6 ] τ7 σ7(MB-Shift0-Ext)
Γ ⊢ S0 k. e : τ1 [τ2 [τ4 σ4 ] τ5 σ5 ] τ3 [τ6 σ6 ] τ7 σ7
図 7. Materzok と Biernacki による shift0/reset0 のための型システム [15]Γ ⊢ e : τ1′ [τ1 σ1 ] τ2′ . . . [τn σn ] τ と書いて、5 「型環境 Γ のもとで MB の項 e を、ある文脈のもとで実行すると最終的に τ 型になる。その文脈は、継続が連なったものであり、それらの型はσ1σnτn となっている」と読める。
τ1′ −→
τ1 , . . . , τn′ −→MB の型注釈の表現の幅を理解するために、簡単な型判断 Γ ⊢ e : τ1 [τ2 σ2 ] τ3 σ3 を例にとって説明する。この型判断の最後の型注釈 σ3 が impure と仮定すると、Γ ⊢ e : τ1 [τ2 σ2 ] τ3 [τ4 σ4 ] τ5 σ5σ2σ4のように展開でき、先ほどのように、τ1 −→τ2 , τ3 −→τ4 という型を持つ継続が連なっていると言える。では、Γ ⊢ e : τ1 [τ2 σ2 ] τ3 σ3 の型注釈 σ2 が impure の場合はどうなるか。σ2 を展開す[τ6 σ6 ] τ7 σ7

ると、Γ ⊢ e : τ1 [τ2 [τ6 σ6 ] τ7 σ7 ] τ3 σ3 と書いて、「τ1 −−−−−−−→ τ2 型の継続のもとで e を実行す
ると最終結果が τ3 型になる」と読める。仮に、残る型注釈 σ6 , σ7 が ϵ だとすると、継続の継続、
つまりメタ継続の型は、直感的には τ1 → (τ2 → τ6 ) → τ7 と言える。
また、図 7 では、λS0 のための型規則を示した。(MB-Var) から (MB-Reset0) までは、文献 [15] からそのまま引用した規則である。(MB-Abs-Ext) は、(MB-Abs) 中の型注釈 σ を展開して [τ3 σ3 ] τ4 σ4 としたものである。また、(MB-Shift0-Ext) は (MB-Shift0) 中の型注釈
σ1 , σ2 を展開してそれぞれ [τ4 σ4 ] τ5 σ5 , [τ6 σ6 ] τ7 σ7 としたものである。これは、λS0 の項において、関数や shift0 の中で仮に pure な部分項があらわれたとき、それを impure であるとみなして、型注釈を冗長に展開したということを意味している。6 このとき、(MB-Abs-Ext) や (MBShift0-Ext) を使って型付けできる項の範囲と、(MB-Abs) や (MB-Shift0) を使って型付けできる項の範囲は同じである。このことは、図 7 の型システムの中で、型注釈が ϵ であることを要求
5
この型判断は本来 Γ ⊢ e : τ1′ [τ1 σ1 ] τ2′ . . . [τn σn ] τ ϵ で、最後の型注釈は ϵ だが、冗長なので省かれている。これ以降の説明や型規則中でも、型注釈が ϵ のときは省略されることが多い。
6
著者らは、関数や shift0 の中には pure な部分項は現れないだろうと考えているが、これについては現在確認中
である。

10

τ

N⇀ m
(τ1 → τ2 ⟨σα ⟩ α ⟨σβ ⟩ β)⇀τmσ(•σ , τ )⇀mσ(((τ1 → ⟨σ1 ⟩ τ2 ) :: σ2 ), τ )⇀mτN⇀ d[τ3 σ3 ] τ4 σ4(τ1 −−−−−−−→ τ2 )⇀dτσ(τ, ϵ)⇀dσ(τ, ( [τ1 σ1 ] τ2 σ2 ))⇀d= Nτ[τ3 σ3 ] τ4 σ4τ= τ1 ⇀m −−−−−−−→ τ2 ⇀m
σwhere (τ3 , σ3 ) = (σα , α)⇀m ,σ(τ4 , σ4 ) = (σβ , β)⇀mτ= (τ ⇀m , ϵ)τ
= (τ1 ⇀m , [τ3 σ3 ] τ4 σ4 )σwhere (τ3 , σ3 ) = (σ1 , τ2 )⇀m ,σ(τ4 , σ4 ) = (σ2 , τ )⇀m

= N
τ

τ

= (τ1 ⇀d ) → (τ2 ⇀d ) ⟨σα ⟩ α ⟨σβ ⟩ βσσwhere (σα , α) = (τ3 , σ3 )⇀d , (σβ , β) = (τ4 , σ4 )⇀dτ= (•σ , τ ⇀d )
τ= (((τ ⇀d → ⟨σ3 ⟩ τ3 ) :: σ4 ), τ4 )σwhere (σ3 , τ3 ) = (τ1 , σ1 )⇀d ,σ(σ4 , τ4 ) = (τ2 , σ2 )⇀d

図 8. 4D と MB の型レベルの変換規則

する型規則がないこと、つまり「必ず pure でなければいけない部分項」を持つ型規則がないことからも明らかだろう。本節において、これ以降、MB と言うとき、(MB-Var), (MB-Abs-Ext),(MB-App), (MB-Shift0-Ext), (MB-Reset0) からなる型システムのことを指すものとする。
ここまでで λS0 の構文やその型規則を眺めてきたが、λD では answer type やメタ継続を使って shift0 の動作を定式化しているのに対して、λS0 では型と型注釈を使って継続やメタ継続をす
べて書き下すことで shift0 の動作を表現している。このように、継続やメタ継続の表記方法が異なるので 4D と MB の型規則の中に現れる型変数どうしを逐一対応付けることは難しいが、4Dの項と MB の項の持つ型を互いに変換することはできそうだ。74.3.2

4D と MB の関係

図 8 に、4D と MB の型レベルの変換規則を定義した。⇀τm , ⇀σm は、4D から MB への変換
で、それぞれ型と型注釈へ変換をおこなう。特に、型注釈への変換 ⇀σm は、4D のメタ継続と、メタ継続を適用した後の answer type の 2 つを与えると、対応する MB の型と型注釈を返すような関数である。また、⇀τd , ⇀σd は、上述の変換の逆変換となっている。ここまでで定めた 4 つの変換規則のあいだには、次のような性質が成り立つ。
τ⇀τ

補題 4.1 λS0 の型 τ1 について、(τ1 ⇀d ) m ≡ τ1 が成り立つ。また、λS0 の型注釈 [τ2 σ2 ] τ3 σ3 に
σ ⇀σ
σ ⇀σ
ついて、(((τ2 , σ2 )⇀d ) m , ((τ3 , σ3 )⇀d ) m ) ≡ ((τ2 , σ2 ), (τ3 , σ3 )) が成り立つ。
□
τ⇀τ

補題 4.2 λD の型 τ について、(τ ⇀m ) d ≡ τ が成り立つ。また、λD のメタ継続 σα と、メタ継σ ⇀σ
続の answer type である α に対して、((σα , α)⇀m ) d ≡ (σα , α) が成り立つ。
□

7

λS0 との変換を考えるのは、λD のうち、「λ 計算と shift0/reset0 のみからなる部分」である。そのため、これ以降で、この節にあらわれる 4D の型では、呼び出し文脈は省略する。

11

これらの補題 4.1, 4.2 が成り立つので、MB で型が付くなら 4D でも型が付くこと、またその逆が成り立つことが言える。その定理を次に示す。また、図 6, 7, 8 やこれらの補題・定理は、いずれも Agda 上で定式化されている。
τ

定理 4.3 λS0 の項 em が MB で Γ ⊢ em : τ1 [τ2 σ2 ] τ3 σ3 であるとする。ここで、τ1 ⇀d = τ かつσσ((τ2 , σ2 )⇀d , (τ3 , σ3 )⇀d ) = ((σα , α), (σβ , β)) のとき、em は、 4D で Γ ⊢ e : τ ⟨σα ⟩ α ⟨σβ ⟩ β であるような λD の項 ed に変換できる。
λD の項のうち λ 計算と shift0/reset0 のみからなる項 e′d が 4D で Γ′ ⊢ e′d : τ ′ ⟨σα′ ⟩ α′ ⟨σβ′ ⟩ β ′τ

であるとする。ここで、τ ′ ⇀m = τ1′ かつ ((σα′ , α′ )⇀m , (σβ′ , β ′ )⇀m ) = ((τ2′ , σ2′ ), (τ3′ , σ3′ )) のとき、e′d は、 MB で Γ′ ⊢ e′m : τ1′ [τ2′ σ2′ ] τ3′ σ3′ であるような λS0 の項 e′m に変換できる。
□

5

σ

σ

Agda による実装

本論文で定義したもののうち、λD や λC の構文 (図 1, 2)、λD から λC への CPS インタプリ
タ (図 3, 4) と、型システム 4D (図 5)、そして λS0 の構文と型システム MB (図 6, 7)、4D と MBの変換 (図 8) と、それらに関連する性質 (補題 4.1, 補題 4.2, 定理 4.3) については、Agda で実装されている。
4D や MB の構文を実装するにあたり、変数束縛には PHOAS [5] を使用している。例えば、
図 4 の λD の CPS インタプリタでは、環境 ρ は実装中には明示的には現れず、PHOAS を使うことで Agda の変数束縛の機能を使って実装されている。

6

関連研究

本論文の 3 節では、著者らの構築した control/prompt の型システム [6] と同様に、Shan の
CPS インタプリタ [18] を η-展開したものをもとに型システムの導出をおこなった。また、このイ
ンタプリタは、Biernacki らによる CPS インタプリタ [3] に等しい。[3] では、control/promptを含む λ 計算のための抽象機械を定義し、それを非関数化することで CPS インタプリタを導出している。
本研究で構築した型システムは、answer type が単相のもののみに対応している。shift/resetの型システムについては、Danvy と Filinski による型システム [7] の answer type が単相である
ため、これを let 多相で拡張し、多相の answer type に対応した shift/reset のための型システ
ムが作られた [1]。また、これをもとに、多相の answer type に対応した control/prompt のための型システムも構築されている [13]。Biernacki と Materzok は、λS0 の型システムとして answer
type が単相の型システム (4.3 節の MB ) を構築し、それに部分型付けを加えることで answer typeが多相の型システムも構築した [15]。
また、近年、代数的エフェクトハンドラ [2] と、継続演算子との関係性を明らかにする試みが多くなされている。中でも、deep handler と shift0、shallow handler と control0 に深い関係があることが知られている [4, 11]。

12

7

まとめと今後の展望

本論文では、shift/reset, control/prompt, shift0/reset0, control0/prompt0 の 4 種類の限定継続演算子のための統一的な型システムを構築し、これを Agda で実装した。また、先行研
究での型システムとの比較をおこない、特に shift0/reset0 の型システムとの対応を証明した。
本研究の型システムは、answer type が単相のものに対応しているため、今後は多相の answer
type にも対応できるように拡張したい。また、この型システムをもとに、代数的エフェクトハン
ドラとの型レベルの関係性を明らかにしたい。

謝辞
有益なコメントをくださった査読者の皆様に感謝申し上げます。また、本研究は一部 JSPS 科
研費 18H03218 の助成を受けたものです。

参考文献[1] K. Asai and Y. Kameyama. Polymorphic Delimited Continuations. Proceedings of the 5th Asian
conference on Programming languages and systems (APLAS’07), pages 239–254, 2007.
[2] A. Bauer and M. Pretnar. Programming with algebraic eﬀects and handlers. Journal of logical andalgebraic methods in programming, 84(1):108–123, 2015.
[3] D. Biernacki, O. Danvy, and K. Millikin. A Dynamic Continuation-Passing Style for Dynamic
Delimited Continuations. ACM Transactions on Programming Languages and Systems (TOPLAS),
38(1):1–25, 2015.
[4] D. Biernacki, M. Piróg, P. Polesiuk, and F. Sieczkowski. Handle with Care: Relational Interpretationof Algebraic Eﬀects and Handlers. Proc. ACM Program. Lang., 2(POPL), dec 2017.
[5] A. Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In Proceedings of the
ACM SIGPLAN International Conference on Functional Programming, ICFP 2008, pages 143–156,
2008.
[6] Y. Cong, C. Ishio, K. Honda, and K. Asai. A functional abstraction of typed invocation contexts. In
6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021),
pages 12:1–12:18, 2021.
[7] O. Danvy and A. Filinski. A functional abstraction of typed contexts. BRICS 89/12, 1989.
[8] O. Danvy and A. Filinski. Abstracting control. Proceedings of the ACM conference on LISP and
Functional Programming (LFP’90), pages 151–160, 1990.
[9] O. Danvy and A. Filinski. Representing control: a study of the CPS transformation. Mathematical
Structures in Computer Science, 2(4):361–391, 1992.
[10] M. Felleisen. The theory and practice of ﬁrst-class prompts. In Proceedings of the 15th ACM
Symposium on Principles of Programming Languages (POPL ’88), pages 180–190, 1988.
[11] Y. Forster, O. Kammar, S. Lindley, and M. Pretnar. On the Expressive Power of User-Deﬁned Eﬀects:
Eﬀect Handlers, Monadic Reﬂection, Delimited Control. Proc. ACM Program. Lang., 1(ICFP), aug
2017.
[12] C. A. Gunter, D. Rémy, and J. G. Riecke. A generalization of exceptions and control in ML-likelanguages. In Proceedings of the 7th International Conference on Functional Programming Languages
and Computer Architecture, pages 12–23, 1995.
[13] Y. Kameyama and T. Yonezawa. Typed dynamic control operators for delimited continuations. In
International Symposium on Functional and Logic Programming, pages 239–254. Springer, 2008.

13

[14] O. Kiselyov. How to remove a dynamic prompt: static and dynamic delimited continuation operators.
Technical Report 611. Indiana University, 2005.
[15] M. Materzok and D. Biernacki. Subtyping Delimited Continuations. In Proceedings of the ACM
SIGPLAN International Conference on Functional Programming (ICFP’11), pages 81–93, 2011.
[16] M. Materzok and D. Biernacki. A Dynamic Interpretation of the CPS Hierarchy. In Asian Symposiumon Programming languages and systems (APLAS ’12), pages 296–311. Springer, 2012.
[17] U. Norell. Towards a practical programming language based on dependent type theory. PhD thesis,
Chalmers University of Technology, SE-412 96 Göteborg, Sweden, September 2007.
[18] C. Shan. A Static Simulation of Dynamic Delimited Control. Higher-Order and Symbolic Computation, 20(4):371–401, 2007.

14