1
日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

Weak HOAS を用いた Featherweight Java とFeatherweight GJ の Coq 上での形式化
奥村 健太郎五十嵐 淳

計算体系を証明支援系上で形式化する際に変数束縛や代入をいかに形式化すると良いかについて長年議論されてきた．
そのなかで，Higher Order Abstract Syntax (HOAS) や weak HOAS と呼ばれる手法が提案されている．HOAS
では，対象言語の変数束縛をメタ言語の関数抽象で表現することで，前述の問題を解決する．Weak HOAS は同様の手法を Coq での形式化にも用いることが出来るようにしたものである．本研究では，オブジェクト指向言語の形
式言語である Featherweight Java (FJ) を weak HOAS を用いて Coq 上で形式化した．また本稿では，FJ にジェ
ネリクスを追加した Featherweight GJ の weak HOAS を用いた形式化についての展望も述べる．

It has been a hot research topic for many years how to formalize variable binding and substitution on a
proof assistant. In the discussion, some formalization styles, e.g. Higher Order Abstract Syntax (HOAS)
and weak HOAS, are proposed. By using HOAS, we can use a function abstraction in the meta language
to represent variable binding. Weak HOAS is a variant of HOAS, which can be used for formalization on
Coq. In our work, we formalize Featherweight Java (FJ), which is a formal language for object-oriented
languages, by using weak HOAS on Coq. Furthermore, we discuss issues in formalization of Featherweight
GJ, an extention of FJ which includes generics, by using weak HOAS.

他の手法に比べて型健全性の証明などの本質的

1 はじめに証明支援系を始め，あるメタ言語を用いて対象言語を形式化しようとする際，変数束縛や α 同値

な作業に集中しやすい• 同じ理由により，形式化が正しく行えているかの検証が比較的容易である

性，代入などをどのように定義，実現するかがし• 名無し表現における名前つけ文脈のような，体ばしば問題となる [1]．その問題を解決するための系の本来の定義には存在しなかった項が付随する手法として，de Bruijn index [7]，locally nameless

ことがなく，これも形式化の正否の検証を容易に[4]，Nameless, Painless [14]，Higher Order Abstract

する

Syntax (HOAS) [12] などの手法がある．
中でも，HOAS はメタ言語の変数束縛や代入を利用して対象言語のそれらを実現する．そのため，他の手法と比べて，以下の様な利点がある．

• 変数束縛，α 同値性，名前変えや代入のための実装をユーザが記述することは不要であるため，
Formalization of Featherweight Java and Featherweight GJ by using weak HOAS on Coq
Kentaro Okumura, 京都大学大学院情報学研究科, Graduate School of Informatics, Kyoto University.
Atsushi Igarashi, 京都大学大学院情報学研究科, Graduate School of Informatics, Kyoto University.

一方，以下の様なことに留意する必要がある．

• 変数束縛や代入の実装の正しさは，メタ言語のそれに完全に依存している点• いくつかの公理が必要となるため，追加した公理が矛盾を引き起こしたり，目的の体系と異なる体系を形式化してしまう可能性がある

HOAS にはいくつかの変種 [9] [5] や応用例 [6] [2] があるが，それらの多くはラムダ計算やそれを拡張した体系の形式化や型健全性の証明，プログラム変換の正当性の証明 [5] に使われる例が多く，オブジェクト指向計算体系の形式化や型健全性の証明に使われるこ日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

2とはなかったと考えている．

型 term は 3 つのコンストラクタを持ち，それぞれ，

本研究では，オブジェクト指向のための形式言語で

Var，Abs，App という名前である．Var は nat 型のある Featherweight Java (FJ) [11](からキャストを項を受けとることで，term の項となる．同様に，Abs取り除いた体系) を HOAS の変種の１つである weakは nat と term の項を受け取ると，App は term の項

HOAS [9] を用いて形式化した．

を 2 つ受け取ると term の項となる．

FJ は HOAS の今までの応用例とは次のような点で異なっている．

これら 3 つのコンストラクタは，上から順に λ 計
算の変数，関数抽象，関数適用を表している．つま• 変数が束縛される構文カテゴリ (メソッド本体

り，この Coq での形式化において，変数は自然数にの仮引数部) と束縛変数が出現する構文カテゴリ

よって表現され，関数抽象は束縛変数を表す自然数と(式の内部) が異なっている点

関数本体を表す λ 項によって構成される．

• 特殊な変数 this の存在
さらに本稿では，FJ にジェネリクス [3] を追加した

ここで，この素朴な λ 項の定義における代入は Coq
でどのように定義されるかを見ていく．

Featherweight GJ (FGJ) [11] の形式化に向けた展望

まず，λ 項の代入は次の 4 つの規則により表される．

についても述べる．FGJ では，現在まで行われてい• [N/x]x = N

る HOAS の応用例や，weak HOAS を用いた FJ の

• [N/y]x = y

形式化と比べて以下の様な点で困難であると予想さ• [N/x](P Q) = ([N/x]P )([N/x]Q)れる．

• [N/x](λy.P ) = λy.([N/x]P )• 型変数の出現はクラス定義内に遍在している• 型変数は再帰的に定義する事ができる(y ̸= x)(x ̸= y and y ∈/ F V (N ))ここで，関数抽象の代入に関する規則に注目されたい．

• 可変個の束縛変数の明示的な出現

この規則では，代入される変数 x と関数抽象の束

本研究の貢献は以下のとおりである．

縛変数 y が異なっており，かつ，y が代入する項 N• Weak HOAS を用いたオブジェクト指向計算体の中に自由に出現しないという条件がある．後者の条系の Coq での初の形式化

件は，N 中の自由変数が代入によって束縛されないようにするためのものである．このような現象は変数

2 HOAS と weak HOAS

捕獲と呼ばれる．また，変数捕獲が起こらないような

本節では，本研究での形式化に用いた weak HOAS

代入は捕獲回避代入と呼ばれる．

とその元となった手法 HOAS について説明する．

前述の条件をみたすために，x と y が同じであった

1 節で述べたように，対象言語の形式化を行う際にり，N 中に y が自由に出現する場合には，関数抽象

変数束縛や α 同値性をどのように扱うかが重要になの束縛変数の名前変えを行わなければならない．名前る．その例として，λ 計算の形式化について考える．

変えを行うためには，フレッシュな変数を用意する必以下に示すのは，λ 計算を証明支援系 Coq で形式化要がある．今，変数は自然数によって表されているたする際の λ 項の素朴な定義である．

め，現在扱っているどの自然数よりも大きな自然数をInductive term : Set :=| Var : nat -> term
| Abs : nat -> term -> term
| App : term -> term -> term.
Inductive は Coq で新しい型や命題を定義するためのもので，ここでは term という新しい型を定義している．

用意すればよい．しかし，そのような変数を用意するには，現在扱われている自然数の最大値を常に把握しておかなければならず，非常に面倒であり，形式化の正しさを検証する上で障害となる．

2. 1 HOAS
HOAS は，対象言語の変数束縛をメタ言語の関数抽象として表現することにより，前述の問題に対処日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集
する．

HOAS では，以下の２つのコンストラクタによって λ 項を表す．

Abs : (term -> term) -> term
App : term -> term -> term
まず注目すべき点は，変数を表すコンストラクタが無いことである．λ 計算の素朴な形式化では，自然数を用いて変数を表現した．しかし，HOAS ではメタ
言語のデータ型 (nat など) の項を使って対象言語の変数を表現する事はしない．
また，関数抽象を表すコンストラクタ Abs は，termを受け取って term を返す関数を引数にとる．メタ言語の関数抽象により，対象言語 (λ 計算) の関数抽象を表現しているのである．

HOAS では対象言語の変数束縛ないし関数抽象を
メタ言語のそれによって表現することから，メタ言語の代入が対象言語の代入に相当する．よって，メタ言
語が捕獲回避代入を正しく実装している限り，対象言語の代入において捕獲回避が正しく行えているかを気にかける必要はない．

HOAS には以上のような利点があるものの，次のような，コンストラクタ Abs と App から構成される型 term を Coq で定義することはできない [13]．

3Inductive term : Set :=| Var : V -> term
| Abs : (V -> term) -> term
| App : term -> term -> term.
一行目の Parameter は Coq において仮定を宣言するためのもので，Parameter V : Set. は識別子 Vが型であることを宣言している．

Weak HOAS を用いた λ 項の定義では，HOAS とは異なり変数項のコンストラクタが存在する．そのコンストラクタ Var は型 V の項を受け取って，型 termの項となる．
また，Abs の型も HOAS と異なっている．Weak

HOAS では対象言語の変数を型 V の項を使って表現するため，関数抽象の引数の型も V になっている．これにより，前節で述べた Coq で定義できない問題を回避することが出来る．

2. 2. 1 weak HOAS での代入の定義
HOAS では，対象言語の変数はメタ言語の term 型の変数によって表現されていたため，メタ言語の代入がそのまま対象言語の代入を表現していた．そのため，ユーザは代入を定義する必要はなかったのである．しかし，weak HOAS では，対象言語の変数は
メタ言語の V 型の変数で表される．そのため，ユー
ザは自分で代入を実装しなければならない．V 型の変Inductive term : Set :=| Abs : (term -> term) -> term
| App : term -> term -> term.
コンストラクタの引数が関数型の場合，その型の”->”数に term 型の項を代入することは出来ないからである．これは，weak HOAS の HOAS と比較したときの欠点であり，これが，”weak” と呼ばれる所以である [10]．

の左に定義しようとしている型を記述することが出Weak HOAS による形式化では，代入を表現する

来ないという制約があるためである．ここでは，Abs

ために次のような形をした三項述語 Sub を定義する．

の引数のドメインに term が出現しているため，このSub (fun x:V=> M) N M’

制約を満たしていない．

この判断は，次のようなことを意味している．

M ′ = [N/x]M
2. 2 weak HOAS
Weak HOAS は HOAS における上記の問題を解決
し，Coq での形式化に対応した手法である．

Weak HOAS を用いた λ 項の定義は次のとおりで

この判断 Sub の直観的な解釈から，Sub の各引数に付いて次のようなことが言える．

• 最初の引数が代入される項を表しており，関数で表現されている．書き換えられる変数はその関ある．

数の引数になっている．x は M 中に自由に出現す

Parameter V : Set.

ることが出来，対象言語の M 中にも x が自由に

日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

4

出現することを表している．

を示している．

• 第二引数，第三引数は関数の形では表されてい3 つ目の SAbs についてであるが，結論部分の第ない．つまり，N や M’ 中には x が自由に出現し一引数，(fun x => Abs ... x) は SApp の結論部分のない事を表している．

(fun x => App (... x) (... x)) と同様のもので，これに以上より，λ 項の代入を weak HOAS を用いて Coqで定義すると次のようになる．

よって λy.P 中の x への代入であることを示している．
また，第三引数は代入後の項が λy.Q であることを示し

Inductive Sub:(V->term)->term->term->Prop:=ている．このとき，yQ は (fun y => ...) の形をした関数抽象である．また，yP は代入しようとしている変数| SVarEq : forall N,

x が自由に出現するため，(fun x => (fun y => ...))Sub (fun x => Var x) N Nの形をしている．次に，SAbs の前提部分についてで| SVarNeq : forall y N,

あるが，ここでは関数抽象の本体を書き換えた時のSub (fun x => Var y) N (Var y)

様子が示されている．SApp のときは前提部分で App| SApp : forall P P’ Q Q’ N,の引数 M と N への代入後の項がそれぞれ M’ と N’ でSub (fun x => P x) N P’ ->あることを示した．同様に，SAbs の前提部分では第Sub (fun x => Q x) N Q’ ->Sub (fun x => App ((fun x => P x) x)((fun x => Q x) x))

一引数と第三引数の Abs の中身を取り出し，それらが Sub によってどのように関係付けられるかを記述したい．Abs の引数 ((yP x) や yQ) は関数抽象になっN (App P’ Q’)ていることから，任意の変数 v : V について，yP x v| SAbs : forall yP yQ N,と yQ v を Sub によって関係づける．また，別の見方(forall v:V,
Sub (fun x => yP x v) N (yQ v)) ->Sub (fun x => Abs (yP x)) N (Abs yQ)をすると，yP x と yQ における束縛変数の名前変えを行っていると考えることも出来る．この結果，前提部
分で Q = [N/x]P であることを示された．

上のコンストラクタから順に，

以上より，SAbs が [N/x](λy.P ) = λy.([N/x]P ) を• [N/x]x = N• [N/y]x = y(y ̸= x)• [N/x](M N ) = ([N/x]M )([N/x]N )• [N/x](λy.P ) = λy.([N/x]P )(x ̸= y and y ∈/ F V (N ))と対応している．

SVarEq の定義の正しさは明らかであることから，表していることが示された．
最後に，SAbs が関数抽象への代入における 2 つの条件を満たしていることを示す．変数 x と y が異なっていることは SVarNeq の時と同様，Coq によって保証されている．また，y が N 中に自由に出現しないことは，yP が (fun x => (fun y => ...)) の形をしていることと，N が yP 中に現れないことから保証される．

これを除く各コンストラクタの定義について見ていくことにする．
まず，SVarNeq についてであるが，ここで登場する

x と y が異なる変数であるというのは，Coq により保証されている．

SApp の 2 つの前提は，それぞれ M ′ = [N/x]M と
N ′ = [N/x]N を意味する．そして，結論部分において 2 つの関数抽象 (fun x => M x) と (fun x => N x)
をそれぞれ外側の束縛変数 x に適用し，それらを Appで結合することで，M N 中の x への代入であること

3 Featherweight Java (FJ) 概要
本節では，本研究で形式化を行った FeatherweightJava (FJ) について，weak HOAS を用いる際に重要となる点を中心に説明する．

FJ はオブジェクト指向言語のための形式言語である．
以下に示すのは，FJ の構文である．上から順にクラス宣言，コンストラクタ，メソッド宣言，式である．
L ::= class C extends C { C̄ f¯; K M̄ }

日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

K ::= C (C̄ f¯) { super(f¯); this.f¯ = f¯ }5ある．

M ::= C m(C̄ x̄ ){ return e; }FJ には式の型付け規則だけでなく，メソッドやク

e ::= x | e.f | e.m(ē) | new C(ē) | (C )e

ラスの well-formedness を推論する規則も存在する．

メタ変数 C はクラスを表し，f はフィールド名，mはメソッド名のメタ変数である．また，x は FJ の変
数のメタ変数である．FJ には特別な変数 this が含まれている．

ここでは，メソッドに関する規則のみ示す．

x̄ : C̄, this : C ⊢ e0 : E0class C extends D { ... }this.f1 = f1 , this.f2 = f2 , ..., this.fn = fn を，C̄ x̄

FJ の簡約規則の内，weak HOAS を用いた形式化の際に重要となるものを以下に示す．

は C1 x1 , C2 x2 , ..., Cn xn を，ē は e1 , e2 , ..., en を表している．
変数はメソッドの仮引数 (メソッド宣言の C̄ x̄) のoverride(m, D, C0 )C0 m(C̄ x̄){ return e0 ; } OK IN C
(T-Method)

メタ変数の上に横線が入っているものは，ゼロ個以上の要素からなる列になっていることを意味
し，C̄ f¯ は C1 f1 , C2 f2 , ..., Cn fn を，this.f¯ = f¯ は

E0 <:C0mbody(m, C) = x̄.e0¯ −→ [d/x̄,¯ new C(ē)/this]e0(new C(ē)).m(d)(R-Invk)

ところで束縛されており，式内部に束縛子はない．λ
計算と FJ との違いのうち，weak HOAS を用いた形

この規則の前提はクラス C のメソッド m の仮引数が式化を行う際に重要となるのは束縛が式の定義の外

x̄ であり，m の返り値が e0 であることを表している．

側にある点である．それが，weak HOAS を用いた形

つまり，この簡約規則はインスタンス new C(ē) のメ

式化にどのように関わってくるかは，4 節で詳しく述

ソッドの仮引数と this にそれぞれ実引数と new C(ē)

べる．

を同時に代入することを意味している．つまり，()以下に示すのは，式の型付け規則である．

x:T ∈Γ
Γ⊢x:TΓ ⊢ e0 : C0

fields(C0 ) = C̄ f¯Γ ⊢ e0 : fi : CiΓ ⊢ e0 : C0

定理 1 (保存). Γ ⊢ e : C かつ e −→ e′ ならば，ある(T-Var)する．

(T-Field)C̄<:D̄
(T-Invk)Γ ⊢ ē : C̄

1. e が new C0 (ē).f を部分式として内包しているならば，ある C̄ と f̄ が存在して，fields(C0 ) = f
かつ f ∈ f¯．

2. e が new C0 (ē).m(d̄ ) を 部 分 式 と し て 内 包Γ ⊢ e0 .m(ē) : CΓ ⊢ fields(C) = D̄ f¯C ′ <:C が存在して Γ ⊢ e : C ′ ．
定理 2 (進行). e は正しく型付けされていると仮定

mtype(m, C0 ) = D̄ → C
Γ ⊢ ē : C̄FJ では以下のような定理が証明されている．

C̄<:D̄

し て い る な ら ば ，あ る x̄ と e0 が 存 在 し て ，mbody(m, C0 ) =x̄ .e0 かつ #(x̄ ) = #(d̄ ) (ただし，#() はリストの要素数を返す関数)．

Γ ⊢ new C(ē) : C(T-New)
上から，変数，フィールドアクセス，メソッド呼び出

定理 3 (型健全性). ∅ ⊢ e : C かつ e −→ e′ (ただし，e′ は正規形) ならば，e′ は値 v で ∅ ⊢ v : D かつ

D<:C ．

し，new 式の型付け規則である．fields 関数はクラス

また，保存の定理の証明に用いられる補題の内，今C0 で宣言されているフィールドとその型の列を返し，

回の weak HOAS を用いた形式化において証明に工mtype 関数はクラス C0 のメソッド m の型を返す．T-

夫を必要としたものを挙げる．

Invk や T-New の ē : C̄ は e1 : C1 , e2 : C2 , ..., en : Cn

補題 1 (代入補題). Γ, x̄ : B̄ ⊢ e : D かつ Γ ⊢ d¯ : Āの，C̄<:D̄ は C1 <:D1 , C2 <:D2 , ..., Cn <:Dn の略記でかつ Ā<:B̄ ならば，ある C<:D が存在して，Γ ⊢日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集6¯[d/x̄]e: C．

今回の形式化では，FJ の変数の集合はあらかじめ FJの型によって分割されていると仮定している．そのこ

4 FJ の weak HOAS を用いた形式化とは V が t にパラメタライズされていることから言4. 1 変数の定義と公理える．したがってこの公理は，任意の型 t について，

まず，FJ の変数を表す型の定義から見ていく．

その型を持つ変数が必ず存在していることを表してParameter V : x this -> Ty -> Set.

いる．
同様に，V vthis t 型の任意の項について命題 P がV は FJ の変数を表現するための Coq の変数である．V は型 x this と Ty によってパラメタライズさ成り立つならば，P を満たす V vthis t 型の項が存在するという仮定も置く．

れている．

Ty は FJ の型を表す Coq の型である．型 x thisAxiom this_exists :forall t (P:(V vthis t)->Prop),

は FJ の特別な変数である this とそれ以外の変数を(forall v : V vthis t, P v) ->区別するためのフラグで，vx と vthis の 2 つのコ

exists v’, P v’.

ンストラクタからなる．このとき，型 V vthis とな
る項は無数に存在しうる．例えば，次のような項を変数 this はクラス毎に異なる型を持つことから，任Coq で記述することが可能である．

意の FJ の型 t について V vthis t 型を持つ項が必ず(fun this1 : V vthis t1 =>(fun this2 : V vthis t2 =>... Var this1 ...
... Var this2 ...

存在すると仮定している．
ここで，任意の型 t について，V vthis t 型の項が唯一であるとは仮定していないことに注意されたい．そのような仮定を置いたとしても，前述の「1 つのクラス中に出現する複数の this が異なる型を持ち)うる」という問題を解決することは出来ないからで)ある．
この項では this の束縛の中に this の束縛が有り，
さらにそれらには別々の型が割り当てられている．このようなことは FJ ではありえない．なぜなら，FJ
では各クラスに対して this の型はただひとつに定ま

4. 2 式の定義
Weak HOAS を用いた FJ の式の定義は以下のとおりである．

るからである．
この問題を解決する方法については，4. 3 節で詳し

Inductive E : Set :=| e var : forall xt t, V xt t -> E

く述べる．

Weak HOAS を用いた形式化では，型 V に関して
いくつかの仮定を置く必要がある．
まず，以下の仮定は「型 V vx t の任意の項につい| fd access : E -> F -> E
| m call : E -> M -> list E -> E
| new : Ty -> list E -> E.

て命題 P が成り立つならば，P を満たす変数が存在

上から順に，変数，フィールドアクセス，メソッ

する (ただし，t は FJ の任意の型)」という公理でド呼び出し，new 式を表している．e var は weakある．

HOAS の手法に従い定義されている．F と M はそれ

Axiom variables_exist :forall t (P : (V vx t) -> Prop),(forall v : V vx t, P v) ->exists v’, P v’.

ぞれ，フィールド名とメソッド名を表す型であるが，FJ においては，フィールド名とメソッド名の束縛は存在しないことから，これらは単純に nat によって実装されている．FJ では変数束縛は式の中に存在し日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集
ないことから，Coq の関数抽象は E の定義内には存
在しない．

7

が必要となる．
さらに，このコンストラクタには，4. 1 節で述べた

this として振る舞う Coq の項が複数存在しうるとい4. 3 メソッド本体における束縛う問題を解決するという目的もある．

前述のとおり，FJ では式の中には変数束縛は現れMB が x this によってパラメタライズされている

ず，変数はメソッド宣言の仮引数部で束縛されていのも同様の理由による．注目すべき点は，関数抽象のる．そのため，メソッドの返り値 e のためのコンスト

型と各コンストラクタの結論の型である．mb empty

ラクタと，変数束縛を表すコンストラクタを用意すと mb var の結論の型はどちらも MB vx である．しる．それに，後ほど説明する mb this というコンス

たがって，mb var の関数抽象の内側には mb empty

トラクタを付け加え，メソッド本体の型 MB は以下のや mb var が出現することができる．また，前述のとように定義される．

おり，mb var を複数回ネストさせることも可能であInductive MB : x_this -> Set :=| mb_empty : E -> MB vx| mb_var : forall t,(V vx t -> MB vx) -> MB vx| mb_this : forall t,(V vthis t -> MB vx) -> MB this.

る．一方，mb this の結論の型は MB vthis である．
よって，mb this が mb var の内側に出現することはない．さらに，mb this の関数抽象の型は V vthist -> MB vx である．したがって，mb this の関数抽象の本体に mb this が来ることはない．これにより，vthis の束縛は型 MB のどの項においても高々１つである．以上より，返り値 e 内に現れる this の型は 1

mb empty は E 型の項を受け取って MB 型の項となる．ここで，この E はメソッドの返り値を表している．

mb var は Coq の関数抽象を用いて変数の束縛を表現するためのものである．FJ では仮引数 (=変数束縛) の数はメソッド毎に異なるため，mb var を複数回ネストさせることにより，任意の数の変数を束縛する

つに定められることになる．
ただし，Parameter などにより変数の宣言を行う
ことが出来るため，厳密には 1 つに定められない場
合が存在する．しかし，coqchk コマンドにより，そのような不正な仮定の有無は検査できることから，問題無いと考えている．

事ができるようにしている．本来，変数束縛はメソッ
ドの仮引数部で複数同時に行われる．しかし，weak

HOAS を用いた手法では関数抽象によって表現する
ため，複数 (かつ可変個の) 変数束縛を同時に行うこ4. 4 式の型判断
式の型判断は以下のとおりである．各コンストラク
タの名前は同名の型付け規則と対応している．

とは非常に困難である．そこでカリー化のように，複数同時になされるべき変数束縛を，関数抽象をネスト

Inductive E_WF : E -> Ty -> Prop :=させる方法で実現している．

| T_Var : forall xt t (v:V xt t),

mb this は this の束縛を表現するためのものであE_WF (e_var v) t

る．本来，メソッド本体は仮引数 x̄ と返り値 e から

| T_Fields : ...

なるため，this の束縛を表現するためのコンストラ| T_Invk : ...

クタがメソッド本体を表す型 MB の定義の中にあるの| T_New : ...

は不適切であると考えられるかもしれない．しかし，特筆すべきは型判断に型環境を表す項が存在しない

this は他の FJ の変数と同様に Coq の変数で表現さことと，T Var の定義である．

れている上，返り値 e 中には this が出現する場合がWeak HOAS の手法では，FJ の変数は Coq の変あるため，その束縛を関数抽象という形で表現しなけ数で表現される．したがって，T Var の引数として変ればならない．したがって，mb this を追加すること数を与えるためには，何らかの形で変数があらかじ8

日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

め Parameter などで宣言されているか，関数抽象において束縛されている必要がある．言い換えると，ある xt:x this と t:Ty について，T Var xt t v という項が構築できたということは，変数 v が V xt t という型として既に (Parameter などで) 宣言させているか，どこかの場所で束縛されていることに他ならな

forall xt, MB xt -> Ty -> Prop :=| wf_e_mb_empty :forall e ty, E_WF e ty ->E_WF_in_MB c x (mb_empty e) ty| wf_e_mb_var :forall t (f : V vx t -> MB vx) ty,

い．このことはまさに，T-Var の前提条件 x : T ∈ Γ(forall v, E_WF_in_MB c x (f v) ty) ->を表していることになる．したがって，V のパラメー

E_WF_in_MB c x (mb_var t f) ty

タ t:Ty がそのまま式 e var v の型になっている．
以上より，weak HOAS を用いた式の型判断は型 Eと Ty によってのみパラメタライズされている．

| wf_e_mb_this :forall (f : V this c -> MB vx) ty,(forall v, E_WF_in_MB c x (f v) ty) ->E_WF_in_MB c this (mb_this c f) ty.

4. 5 式の型判断の拡張
4. 4 節では，型付けされる式の中に登場する (Coqの) 変数は既に宣言されているか，どこかで束縛されている前提で式の型判断 E WF の定義についての議論を進めた．本節では，変数を束縛して式の型判断を行
うための型を定義する．
その型をどのように定義すればよいかは，次のような手順で見ることが出来る．
まず，FJ の定義において，式の型判断は T-Method

wf e mb empty は仮引数がないメソッドにおける式
e の型判断つまり，⊢ e : T を表している．
wf e mb var は，1 つ以上の仮引数が存在するメ
ソッド に お け る 返 り 値 の 型 判 断 を 表 現 し て い る ．

wf e mb var の引数 f は，4. 3 節で述べた，メソッ
ド本体における変数束縛を表現するための関数抽
象 で あ る ．こ の コ ン ス ト ラ ク タ の 前 提 部 分 で は ，

2. 2. 1 節の SAbs と同じく，関数抽象 f の本体を参照するために V vx t 型の変数 v に f を適用してい中に x̄ : C̄, this : C ⊢ e0 : E0 の形で現れる．ここる．SAbs では前提部分で関数抽象の本体同士を Sub

で，e0 はメソッドの返り値であり，x̄ : C̄ はメソッドで関連付けが，ここではより束縛が少なくなったの仮引数とその型を表してる．また，4. 4 節では，ある xt と t について，変数 v:V xt t が既に宣言されていたり束縛されているということは，FJ の型環境
中に v:t があることと同義であると述べた．さらに，

4. 3 節で見たように，MB のコンストラクタ mb var とmb this 中の関数抽象によってメソッドの仮引数とthis の束縛が表現されており，mb empty の引数はメソッドの返り値を表している．
以上のことから，型 MB の項の中に含まれているメ
ソッドの返り値と仮引数や this の束縛，Coq の変数
束縛と FJ の型環境との関係性，そして，E WF の定義から，x̄ : C̄, this : C ⊢ e0 : E0 の導出を表現する

Coq の閉じた項を記述することができるようになる．
それを実現するのが以下に示す E WF in MB である．

メソッド本体 f v において，メソッドの返り値が型

ty になることを表す判断 E WF in MB c x (f v) ty
を 前 提 と し て い る ．．こ こ で 注 目 す べ き は ，(forall v, E WF in MB c x (f v) ty) の 項 は 関
数抽象になっている点である．つまり，変数 v が型 V vx t を持っているという仮定のもとに，判断

E WF in MB c x (f v) ty が導出されることを前提にしている．4. 4 節での議論より，これは，FJ の型
環境に v:t があることと同義であった．以上のことから，wf e mb var はメソッドの変数束縛を元に，式の型判断の仮定を作り出していることが分かる．

wf e mb this は ，wf e mb var と 同 様 の こ と を
vthis に対して行うものである．
前節で見たように，MB の定義では vthis の変数束
縛が一番外側に高々１つ来ることが出来るよう型が工Inductive E_WF_in_MB (c:Ty) :夫してある．したがって，MB の型と E WF in MB の定日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集
義より，vthis の型が 2 つ以上仮定されるようなこと

9e (fd_access e0’ f)

はない (これも，4. 3 節で述べた時と同様，Parameter| S_m_call : ...

で破ることは可能であるが，問題ない)．

| S_new : ...
weak HOAS を用いた λ 項の式と同様，命題として

4. 6 メソッドの型判断定義されている．Sub の第一引数は V から E への関メソッドの型判断 T-Method は以下の Meth WF により表される．

数になっており，V が現在注目している変数である．
そして，第二引数が代入される項，第三引数が代入後Inductive Meth_WF : C -> MD -> Prop :=| T_MD : forall (mb:MB vthis) (E_0 C_0 :Ty)の項を表している．

FJ では変数への代入は，メソッドの仮引数への実(c:C) (m:M) ...,

引数の代入と this への new C(ē) の代入がある．3

E_WF_in_MB (cl c) vthis mb E_0 ->節で述べたように，複数ある仮引数と this への代入...

は同時に行われる．しかし，上で定義した判断 Sub

Meth_WF c (md C_0 m mb).

は式への単独の代入しか表現できていない．したがっこれまでの議論の結果から，Meth WF について以下のて，メソッドの仮引数と this への同時代入を表現するための述語が必要となる．それが以下の述語 Subst

様なことが言える．
まず，mb は型 MB であることから，仮引数 x̄ とその型 C̄ の情報を関数抽象の形で保持しており，一番である．

Inductive Subst : forall xt, MB xt ->内側の関数抽象の本体がメソッドの返り値 e となっている．したがって，Meth WF c (md c 0 m mb) は，

list E -> E -> Prop :=| Sub_empty : forall e,

T-Method の結論部分に一致していることが分かる．

Subst _ (mb_empty e) nil e

さ ら に ，E WF in MB の 第 二 引 数 が vthis に な| Sub_var : forall t f es e e0 e’,って い る こ と か ら ，前 節 で の 議 論 よ り，こ れ はx̄ : C̄, this : C ⊢ e0 : E0 を表していることが分
かる．

(forall v : V x t,
Subst _ (f v) es (e x t v)) ->Sub e e0 e’ ->以上より，weak HOAS を用いた手法によって，Meth WF は (少なくとも，メソッドの本体の型付けに関して) T-Method を正しく形式化できていると言える．

Subst _ (mb_var _ f) (e0::es) e’| Sub_this : ...
Subst の MB xt は，代入が施されるメソッド本体を表している．前節では判断 x̄ : C̄, this : C ⊢ e0 : E0
を形式化するためにメソッドの変数束縛を利用した

4. 7 代入が，ここでは e = [d̄ /x̄ , new C (ē)/this]e0 を形式化

FJ における式の代入の定義は以下のとおりである．
Inductive Sub : (forall xt t, V xt t -> E) ->E -> E -> Prop :=するためにメソッドの変数束縛を利用する．
前述のとおり，本来ならばこれらの変数への代入を同時に行わなければならない．しかし，Weak HOAS

| S_var_eq : forall e, Sub e_var e eを用いた手法では，項 T 中の変数 x を書き換えよう| S_var_neq : forall xt t (v:V xt t) e,としている事を (fun x => T) という形の関数抽象で

Sub (fun _ _ _ => e_var v) e (e_var v)| S_fd_access : forall e0 e e0’ f,

表現するため，複数の変数への代入を同時に行うことは出来ない．これは，4. 3 節で述べた，メソッドにおSub e0 e e0’ ->ける変数束縛の複数同時に関する問題と同様のもの

Sub (fun ... => fd_access (e0 xt t v) f)

である．したがって，Subst においても関数抽象のネ日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

10

ストによって表現された仮引数と this の束縛から代入のための項を作り出す操作をしている．
変数への代入を同時に行わなくても良い理由としては，weak HOAS では，変数捕縛がメタ言語の機能
により自動的に回避されるため，1 つずつ代入を行っても，同時代入と同じ項を得ることが出来るためである．

題の文言は少し複雑である．

Lemma Term subst pres types :forall mb D0 D, E WF in MB D0 this mb D ->forall ds Ss Us e,
List_P2’ E WF ds Ss ->List_P2’ subtype Ss Us ->Extract_tys this mb Us ->Subst this mb ds e ->4. 8 簡約規則の定義

exists E, E WF e E /\ subtype E D.

Subst を使って，簡約規則の定義は以下の様に定義できる．

List P2’ は二項述語を 2 つのリストに適用できるよ
うにするためのもので，帰納的に定義された命題であInductive Reduce : E -> E -> Prop :=る．判断 List P2’ P l1 l2 において l1 と l2 の長| R_Field : forall c ty fds es f e n, ...

さは同じになるように定義されている．

| R_Invk : forall m c (mb:MB vthis) es ds e,

Extract tys はメソッドの仮引数の型を取り出す

mbody m c mb ->ための述語である．これは，Subst や E WF in MB と

Subst vthis mb (new c es::ds) e ->同様に，MB の構造に関して帰納的に定義されている．

Reduce (m_call (new c es) m ds) e.

よって，代入補題は MB の構造に関する帰納法によっ

Subst の第一引数が vthis になっていることから，て証明される．ここで，induction step において次のvthis への代入が存在することが分かる．したがっように定義される命題を用いた．

て，e = [d̄ /x̄ , new C (ē)/this]e0 (ただし，e0 は mbの返り値) であり，R-Invk が正しく形式化されていることが分かる．

Definition
Term_subst_pres_types_sub_P
e0 d e (sub_e0 : Sub e0 d e) :=forall xt t (v:V xt t) D S,

4. 9 FJ の性質の形式化
本節では 3 節で紹介した FJ の性質の内，weak

HOAS を用いた形式化と関連の深い，保存と代入補

E_WF (e0 _ _ v) D ->E_WF d S ->subtype S t ->題の文言がどのように形式化されるのかについて述

exists C, E_WF e C /\ subtype C D.

べる．
まず，保存の文言は次のように形式化される．3 節の保存の文言と比べると，非常に自然な形式化である
ことが分かる．

こちらの命題のほうが代入補題の本質的な部分を表していると言える．前述の Term subst pres types
は複数の代入に対する補題であったが，こちらは単独の代入に関する補題である．こちらの補題は，Sub のTheorem preservation :forall e e’, Reduce e e’ ->forall c, E_WF e c ->導出に関する帰納法によって証明される． [11] において，代入補題は型判断の導出に関する帰納法によって証明されているとは対照的である．

exists d, E_WF e’ d /\ subtype d c.
ここに出てくる式の型判断は 4. 4 節で定義したものである．
この保存の定理を証明するのに用いられる代入補

5 Featherweight GJ (FGJ) の形式化に向けて
本節では現在取り組んでいる Featherweight GJ

日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集(FGJ) の形式化について述べる．

11

X とその上限 N のリストから成る．X̄<:N̄ と Ȳ <:P̄はそれぞれクラス C とメソッド m の型変数とその上

5. 1 FGJ 概要

限を表している．∆ ⊢ T ok は型環境 ∆ のもとでの

FGJ は FJ にジェネリクスを追加した体系である．

型 T の well-formedness を表す判断である．

以下に示すのは，FGJ の構文である．上から順に，型，非変数型，クラス宣言，コンストラクタ，メソッ
ド宣言，式である．

また，以下にクラスの型判断 GT-Class を示す．

X̄<:N̄ ⊢ N̄ , T, T̄ okfields(N ) = Ū ḡ

M̄ OK IN C⟨X̄ ◁ N̄ ⟩K = C(Ū ḡ, T̄ f¯){super(ḡ); this.f¯ = f¯; }T ::= X|N
N ::= C⟨T̄ ⟩L ::= class C⟨X̄ ◁ N̄ ⟩ ◁ N {T̄ f¯; K M̄ }K ::= C (C̄ f¯) { super(f¯); this.f¯ = f¯ }M ::= ⟨X̄ ◁ N̄ ⟩ T m(T̄ x̄) { return e; }e ::= x | e.f | e.m⟨T̄ ⟩(ē) | new N (ē) | (N )e
メタ変数 T は型を表し，X は型変数，N は非変数型のメタ変数である．それ以外のメタ変数の意味は FJと共通である．また，⟨X̄ ◁ N̄ ⟩ は ⟨X1 ◁ N1 , X2 ◁ N2 ,..., Xn ◁ Nn ⟩ の略記である．

class C⟨X̄ ◁ N̄ ⟩ ◁ N {T̄ f¯; K M̄ } OK
(GT-Class)
ここで注目すべきなのは，判断 M̄ OK IN C⟨X̄ ◁ N̄ ⟩である．これは，M1 OK IN C⟨X̄ ◁ N̄ ⟩, M2 OK IN

C⟨X̄ ◁ N̄ ⟩, ..., Mn OK IN C⟨X̄ ◁ N̄ ⟩ の略記で，クラス C で宣言されている全メソッドが well-formed であることを意味している．

FGJ でも FJ と同様に， [11] で型健全性が証明され

FGJ ではジェネリクスを扱うために型変数が導入ている．

される．型変数はクラス宣言 L やメソッド宣言 M において宣言され，L や M 中に自由に出現することが出来る．クラス宣言やメソッド宣言中の X̄ がその束縛を表している．型変数には上限となる型があり，型変数はその部分型の範囲を動く．型変数 X の上限がN であることを，X ◁ N と書き表す．型変数 X の上限
は他の型変数ではなく，非変数型 N でなければならな
いが，この上限の一部に X 自身や他の型変数が現れ

5. 2 FGJ の形式化の際に工夫が必要となる点
本節では，weak HOAS を用いて FGJ を形式化す
る際に，工夫が必要となる点や問題となる点について述べる．

5. 2. 1 型変数の上限の取り扱い
FGJ の型変数は束縛があるため，一般の変数と同様に weak HOAS を使って形式化する際には，そのることは可能である．つまり，⟨X ◁ C⟨X⟩⟩ と定義す

束縛を Coq の関数抽象を使って表現することになる．

ることも出来る．さらには，⟨X ◁ C⟨Y ⟩, Y ◁ C⟨X⟩⟩

そのために，V と同様のパラメータ TV を用意する．

の様に型変数を再帰的に定義することも可能である．
以下に示すのはメソッドの型判断 GT-Method である．

変数に関しては，4. 1 節で述べたように，V を Ty
でパラメライズすることにより，変数に型の情報を付随させることが出来た．それと同様に，型変数を表現∆ = X̄<:N̄ , Ȳ <:P̄∆ ⊢ T̄ , T, P̄ ok∆; x̄ : T̄ , this : C⟨X̄⟩ ⊢ e0 : S∆ ⊢ S<:T

する Coq の型 TV をその上限の型，すなわち Ty，によってパラメタライズすると型変数を表す Coq の変class C⟨X̄ ◁ N̄ ⟩ ◁ N {...}

数に上限の情報を付随させることが出来，都合が良override(m, N, ⟨Ȳ ◁ P̄ ⟩T̄ → T )いと考えられる．しかし，前節で述べたとおり，FGJ⟨Ȳ ◁ P̄ ⟩ T m(T̄ x̄){ return e0 ; } OK IN C⟨X̄ ◁ N̄ ⟩(GT-Method)の型変数が再帰的に定義される可能性があるため，そのような手法を用いることが出来ない．例えば，

class C⟨X ◁ D⟨Y⟩, Y ◁ D⟨X⟩⟩ ◁ D { ... }メタ変数 ∆ は型変数の型環境を表しており，型変数のようなクラス宣言を表すために，

日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

12

c_decl C (fun X : TV (D Y) =>(fun Y : TV (D X) => ...))のような Coq の項を書こうとしても，型変数 X の上
限 D⟨Y⟩ 中に出てくる型変数 Y は，その後ろで束縛されているため，エラーになってしまう．
そこで，TV を Ty でパラメタライズする方法は採らずに，型変数の上限を以下のようにリストとして明示的に保持することにする．

5. 2. 2 型変数の束縛と代入
FGJ では，型変数の束縛がクラス定義とメソッド定義の両方に現れる．クラス定義において束縛された型変数は，そのクラス全体に自由に出現し，メソッ
ド定義における束縛された型変数は，メソッド全体に出現することが出来る．そのため，FJ の形式化の際に定義した Subst のような述語を多数定義する必要がある．
例えば，以下のクラス宣言において束縛される型

Definition Bnd_first_def := list N.

変数 X̄ は，X̄ の上限 N̄ ，親クラス N ，フィールド

つまり，型変数とその上限のリスト X̄ ◁ N̄ を，複数変数の型 T̄ ，コンストラクタ K そしてメソッド宣言の型変数の束縛を表す (ネストした) 関数抽象とそれらの上限を表す Ty 型のリストの 2 つに分けて形式化

M̄ の全てに出現することが出来る．
L ::= class C⟨X̄ ◁ N̄ ⟩ ◁ N {T̄ f¯; K M̄ }するという方法を採る．ここで，X̄ と N̄ を切り離し

そして，それぞれのオブジェクト中に出現する X̄ へて形式化したため，それらを関係付けるための仕組みの代入を定義する必要がある．したがって，形式化がが必要である．そこで，型変数を表す Ty 型と上限の正しく行えているかの検証の際に，それら複数の代入

リストそれぞれに，どのクラス，あるいはどのメソッの定義が正しいかどうかを判断する必要があり，検証

ドで宣言された型変数やその上限であるかを示すたの容易性を多少損なってしまうという問題がある．

めの情報を追加する．よって，上限を表すリストは以5. 2. 3 GT-Method における束縛

下のようになる．

FGJ の weak HOAS を用いた形式化の内，最大

Definition Bnd := list (N*C*option M).
ここで，C は型変数が宣言されたクラスを表す．option

M は，型変数が宣言されたメソッドを表しており，型
変数がクラス宣言において宣言されたものである場
合は，None になる．同様に，型 TV は型変数が宣言されたクラスとメソッドを表すために，型 C と option

M によってパラメタライズされ，さらに，上限がリス
トのどの要素であるかを表すために，nat によってもパラメタライズされる．つまり，Parameter TV : C -> option M -> nat -> Set.と定義する．
この定義に基づいて前述のクラス宣言 c decl は次のように書き直される．

c_decl C(fun X : TV C None 0 =>(fun Y : TV C None 1 =>[(D Y, C, None); (D X, C, None)]...
))の問題であると考えているのが，メソッドの型判断

GT-Method の形式化である．特に，返り値の型判断，∆; x̄ : C̄, this : C⟨X̄⟩ ⊢ e0 : E0 の中に型変数 X̄ をどのように形式化すべきかが問題となっている．
この問題の詳細に立ち入る前に，まず GT-Method
全体を Coq のどのような型で表すべきかについて説明する．繰り返しになるが，GT-Method はメソッドの型判断である．M OK IN C⟨X̄ ◁ N̄ ⟩ という判断は，クラス C⟨X̄ ◁ N̄ ⟩ のもとでメソッド M は well-formedであることを意味している．ここで，C⟨X̄ ◁ N̄ ⟩ はGT-Method 内に出現する型変数 X̄ の束縛子であると考えられる．FGJ のクラスの型パラメータの個数は可変であることから，X̄ の個数も可変である．したがって，MB と同様に，GT-Method を表す Coq の型 GMeth WF は，GT-Method の前提条件を形式化したコンストラクタ gm wf と，型変数の束縛を表す関数抽象を引数にとるコンストラクタ gm wf tp からなる inductive type として定義すると良い．そして，

gm wf tp をネストさせることによって可変個の X̄ の束縛を表すことが出来る．

日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

13

では，∆; x̄ : C̄, this : C⟨X̄⟩ ⊢ e0 : E0 中に現れ

Autosubst Coq における名前変えや代入を取りる X̄ はどのように形式化されるべきだろうか．X̄ の扱うためのライブラリとして，Autosubst [15] と呼ば個数も可変であることから，X̄ を TV のリスト (名前れるものがある．Autosubst は de Bruijn index [7] にを Xs とする) を使って表現することが望ましいと考基づいており，型を定義するときに，どのコンストラ

えられる．ここで，リスト Xs が gm wf tp で束縛さクタが束縛子を表しているかをユーザが指定することれた型変数を過不足無く含んでいることを示さなけが出来る．さらに，Instance というキーワードを用ればならない．１つの方法としては，gm wf tp を以いると，型を定義した時に指定した束縛子の情報を元下のように定義することである．

に，自動的に代入や名前変えなどの関数を生成する．

gm wf tp : forall m c Xs Ns,(forall X:TV ...,
GMeth WF m c (X::Xs) Ns) ->GMeth WF m c Xs Ns

現段階では，Autosubst と FJ や FGJ との相性は未知数である．

7 おわりに
7. 1 結果と考察

このコンストラクタでは，束縛された変数をリスト

Xs に追加している．これにより，gm wf 中の Xs の個数は束縛された型変数を必ず含んでいることになる．
そして，判断 GT-Method が登場するクラスの型判
断 GT-Class おいて，GMeth WF m c nil Ns とすることで，GT-Method において束縛されていない変数
は Xs 中に含まないことが保証される．
現在はこのような方針で型健全性の証明を進めている．

6 関連研究Parametric HOAS Weak HOAS を発展させた手法に Parametric HOAS (PHOAS) [5] と呼ばれるものがあり，いくつかの応用例がある [8] [6] [2]．

PHOAS と weak HOAS との違いは主に以下の２つである．

• Weak HOAS では変数の型 V は Parameter として定義されたが，PHOAS では V を型パラメー
タとして term などの型を定義する• 代入の定義など，対象言語の項に関する操作を定義する際に，型パラメータ V を具体化する

PHOAS は this の型にまつわる問題を解決するには非常に有用であると考えられる．しかし，PHOAS によるカリー流の型付けを Coq 上で形式化する手法はまだ確立されていない．FJ はカリー流の型付けであるため，本研究での形式化には用いることが出来なかった．

本研究では Featherweight Java を weak HOAS を用いて形式化した．Weak HOAS は今まで，オブジェ
クト指向向けの形式化で用いられたことはなかった
が，今回， [9] で用いられていた手法とほぼ同じで FJを形式化することが出来た．その際，以下の点で工夫が必要であった．

• 特別な変数 this の取り扱い
Weak HOAS では変数は Coq の型 V で表されるため，this とそれ以外の変数とを区別するために V を x this でパラメタライズした．そのことにより，あるクラス内において this に複数の型が付き得るという問題が発生した．本研究では，MB の型定義を工夫することによりこの問題を解決した．また，Parameter による仮定でthis に複数の型を付けることができるが，それは，coqchk を用いて検査することが出来る．
また，FGJ については以下の様な工夫点が必要となる．

• 型変数の取り扱い
FGJ の型変数は再帰的に定義できることから，型変数とその上限の型を切り分けて形式化しなければならない．前者は TV 型をドメインに持つ
関数抽象で，後者はリストによって表現される．

• 可変個の型変数の形式化
GT-Method において型変数の可変個の列が出現する箇所があり，これをどのように形式化するかが問題となっている．個数が可変であること

日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

14から，TV 型のリストによって表現すると良いが，

GT-Method の結論部分において束縛された型変数が過不足無くリストに含まれている事を示す必要がある．現在は，GT-Method における型変数の束縛を表すコンストラクタ gm wf tp において，束縛された変数をリストに追加する，という方針
で型健全性の証明を進めているところである．

Weak HOAS ではユーザが代入を実装する必要があり，全く実装する必要のなかった HOAS と比べて欠点といえる．しかし，HOAS 系以外の手法と比べると，代入の定義は直観的であり，補助的な関数なども必要としない．したがって，形式化の正否を検証する際には大きな障害にはならないと考えている．

7. 2 今後の課題
今後の課題としては，FGJ の型健全性の証明を完成させることである．
さらに，Autosubst を用いて FJ や FGJ を形式化
し，どのような利点や問題点があるかを検証し，weak

HOAS を用いた形式化との比較を行う．
また，PHOAS を用いてカリー流の型付けを形式化する手法はまだ確立されていないことから，PHOAS
を用いたカリー流の型付けの方法を考案することも今後の課題として挙げられる．

参 考 文 献[ 1 ] Brian E. Aydemir, Aaron Bohannon, Matthew
Fairbairn, J. Nathan Foster, Benjamin C. Pierce,Peter Sewell, Dimitrios Vytiniotis, Geoﬀrey Washburn, Stephanie Weirich, and Steve Zdancewic.
Mechanized metatheory for the masses:
The
PoplMark challenge. In TPHOLs, pages 50–65,
2005.
[ 2 ] Patrick Bahr and Tom Hvitved. Parametriccompositional data types. In MSFP, pages 3–24,
2012.
[ 3 ] Gilad Bracha, Martin Odersky, David Stoutamire,
and Philip Wadler. Making the future safe forthe past: Adding genericity to the Java Programming Language. In Proceedings of the 13th ACM
SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA ’98, pages 183–200, New York, NY, USA, 1998.
ACM.

[ 4 ] Arthur Charguraud. The locally nameless representation. J. Autom. Reasoning, 49(3):363–408,
2012.
[ 5 ] Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In Proceedings of the 13th ACM SIGPLAN International
Conference on Functional Programming, ICFP ’08,
pages 143–156, New York, NY, USA, 2008. ACM.
[ 6 ] Bruno C. d. S. Oliveira and William R. Cook.
Functional programming with structured graphs.
In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming,
ICFP ’12, pages 77–88, New York, NY, USA, 2012.
ACM.
[ 7 ] Nicolas de Bruijn. Lambda-calculus notation
with nameless dummies: a tool for automatic formula manipulation with application to the ChurchRosser theorem. Indag. Mathe., pages 381–392,
1972.
[ 8 ] Benjamin Delaware, Bruno C. d. S. Oliveira,and Tom Schrijvers. Meta-theory à la carte. In
Proceedings of the 40th Annual ACM SIGPLANSIGACT Symposium on Principles of Programming
Languages, POPL ’13, pages 207–218, New York,NY, USA, 2013. ACM.
[ 9 ] Joëlle Despeyroux and André Hirschowitz.
Higher-order abstract syntax with induction in coq.
In Proceedings of the 5th International Conference
on Logic Programming and Automated Reasoning,
LPAR ’94, pages 159–173, London, UK, UK, 1994.
Springer-Verlag.
[10] Furio Honsell, Marino Miculan, and Ivan
Scagnetto. The theory of contexts for first order andhigher order abstract syntax. Electr. Notes Theor.
Comput. Sci., 62:116–135, 2001.
[11] Atsushi Igarashi, Benjamin C. Pierce, and Philip
Wadler. Featherweight Java: A minimal core calculus for Java and GJ. ACM Trans. Program. Lang.
Syst., 23(3):396–450, 2001.
[12] Frank Pfenning and Conal Elliott. Higher-orderabstract syntax. In Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language
Design and Implementation, PLDI ’88, pages 199–
208, New York, NY, USA, 1988. ACM.
[13] Frank Pfenning and Christine Paulin-Mohring.
Inductively defined types in the Calculus of Constructions. In Proceedings of the 5th International
Conference on Mathematical Foundations of Programming Semantics, pages 209–228, London, UK,
UK, 1990. Springer-Verlag.
[14] Nicolas Pouillard. Nameless, painless. In Proceedings of the 16th ACM SIGPLAN International
Conference on Functional Programming, ICFP ’11,
pages 320–332, New York, NY, USA, 2011. ACM.
[15] Steven Schäfer and Tobias Tebbi. Autosubst.
https://www.ps.uni-saarland.de/autosubst/.