\chapter{プログラミング言語の検証}
\label{chapter:intro}
現在の OS やアプリケーションの検証では、実装と別に検証用の言語で記述された実装と証明を持つのが一般的である。
実際に kernel 検証を行った例\cite{Klein:2010:SFV:1743546.1743574} \cite{Nelson:2017:HPV:3132747.3132748}
では C で記述された Kernel に対して、検証用の別の言語で書かれた等価な kernel を用いて OS の検証を行っている。
また、別のアプローチとして ATS2\cite{ats2} や Rust\cite{rust} などの低レベル記述向けの言語を
実装に用いる手法が存在している。

定理証明支援向けのプログラミング言語としては Agda\cite{agda}、 Coq\cite{coq} などが存在しているが、
これらの言語自体は実行速度が期待できるものではない。

そこで、当研究室では検証と実装が同一の言語で行う Continuation based C\cite{kaito-lola} (CbC) という言語を開発している。

CbC では、処理の単位を CodeGear、 データの単位を DataGear としている。
CodeGear は値を入力として受け取り出力を行う処理の単位であり、 CodeGear の出力を 次の GodeGear に接続してプログラミングを行う。 CodeGear の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行うことができる。
このメタ計算部分で検証を行うことで、 CodeGear の処理に手を加えることなく検証を行う。

本研究では Agda 上で CodeGear、DataGear という単位を用いてプログラムを記述し、
メタ計算部分で Hoare Logic を元にした検証を行った。