--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/main.tex	Mon Apr 17 11:49:31 2023 +0900
@@ -0,0 +1,74 @@
+\documentclass[twocolumn]{article}
+\usepackage{luatexja}
+\usepackage{fontspec}
+\usepackage{graphicx}
+\usepackage{float}
+\restylefloat{figue}
+\pagestyle{empty}
+
+%\hoffset -1in \addtolength{\hoffset}{20mm}
+%\voffset -1in \addtolength{\voffset}{20mm}
+%\oddsidemargin 0mm
+\topmargin -4mm
+%\headheight 13pt
+%\headsep 15mm
+%\textheight 43\baselineskip \addtolength{\textheight}{\topskip}
+%\textwidth 160mm
+%\marginparsep 3mm
+%\marginparwidth 15mm
+%\footskip \headsep
+\input usepackage.tex
+\begin{document}
+\setmainfont{STIX Math}%
+\setmonofont{STIXGeneralBol}[
+  Scale=MatchLowercase
+] % or whatever font you prefer
+
+\ltjsetparameter{jacharrange={-3}}
+
+% \input tgrindfig.tex
+\bibliographystyle{plain} % for bibliography
+%
+\include{title}
+%\title{}
+% 英文のみのタイトルならば，\title{ ... } とする．
+
+\date{}
+
+% 所属ラベルの定義
+
+% 和文著者名
+\author{
+{河野真治} \\
+琉球大学工学部\\
+{Shinji KONO} \\
+Faculty of Engineering, University of the Ryukyus\\
+}
+
+\maketitle{}
+\thispagestyle{empty}
+\begin{abstract}
+\input{abstract}
+\input{abstract-e}
+\end{abstract}
+
+% {\em 概要 \vspace{0.5cm}}\
+%\begin{center}
+%{\Large
+%\include{title-e}\
+%\include{author-e}} % \hspace{0.7cm}
+%\end{center}
+
+% {     t \Large Abstract}\
+%\include{abstract-e}
+% \\
+% \hspace{0.5cm}
+
+%
+\input 0.tex
+%
+% \input reference.tex
+
+\bibliography{ref}
+\end{document}
+

--- a/rbtree.ind	Sat Apr 15 13:05:51 2023 +0900
+++ b/rbtree.ind	Mon Apr 17 11:49:31 2023 +0900
@@ -4,9 +4,47 @@
 
 --abstract:
 
+GearsAgdaではHoare LogicをAgda上に実装することよによりBinaryTreen
+の検証を可能のした。これをRedBlack Tree さらに、その木に対
+する並行実行の検証に拡張したい。invariantを拡張することによ
+り、Red Black Treeの検証を行う。並行実行は、Model 検査をGeas
+Agda上で形式化することにより実現する。これについて考察を行う。
+
 --検証された Red Black Treeの重要性
 
-OSを含むアプリケーションの
+OSを含むアプリケーションの信頼性は、当然、OSのアプリケーションの両方の信頼性を上げる必要がある。
+信頼性を上げる手法には、テストやモデル検査などがあるが、数学的な証明を行うことが基本である。
+
+最近では、定理証明を高階直観論理あるいは高階関数型言語で行うことができる。これは、Curry Howard
+対応\cite{currey-howard}と呼ばれる命題と型の対応、そして、推論と関数の対応があるためである。実際には、
+Curry Howard 対応が、高階直観論理の意味を決めるのを主導していくことになる。例えば Coq \cite{coq}やIsabel HOL\cite{isabel}
+そして、本論文で使用するAgda \cite{agda}が知られている。
+
+一般的なプログラムにはループや再帰呼び出しがあり、メモリや並行実行などと関連している。
+メモリや並行実行あるいはI/Oは、プログラムの関数としての性質とは直接は関係しないので、
+副作用と呼ばれることもある。これらを理論的に扱う手法としてMonadがある。
+Monad \cite{monad} は通常の関数にメタ情報を扱う構造を付加する方法になる。
+
+OSを含むアプリケーションは、証明を意識した手法でプログラミングされるべきであり、
+一つの方法は、すべてをリストのような特定の型変数を含むデータ構造(関手)として
+定義して、そのmapとしてプログラムを記述することである。これにより圏論的な
+証明手法(交換図)が使えるようになる。この方法は有効だが一般的とは言えない。
+例えば、バランス木の一種であるRed Black Treeのinsert操作はmapではなくて、
+構造変化させる操作なので、その操作の正しさは関手による方法で書くことは
+自明にはならない。
+
+このような場合に有効なのは invariant (ループや再帰で不変な条件/命題)を見つけることであり、
+古典的には Hoare Logic として知られている。この論文では、実際に、簡単な while program
+の証明と、二分木、そして Red Black Tree \cite{red-black-tree}のinvariantについて考察する。
+
+GearsAgda \clite{gearAgda}は、Gears OS\cite{gearsos}に採用されている CbC (Continuation based C)\cite{cbc}をAgdaで記述する
+方法である。これを用いることにより、CbCに直接対応した Hoare Logic よりも柔軟な
+証明法を使うことができる。例えば、プログラムの停止性は、CbCの実行単位である
+Code Gearに対して、ループで減少する自然数を対応させることで容易に示すことが
+できる。これは、Code Gearの接続子(loop connector)のようなものになる。
+
+また、並列実行も Code Gear単位のシャッフルと考えることにより、モデル検査的な証明が
+可能になる。この方についても考察する。
 
 --CbCに証明を付け加えた GearsAgda
 
@@ -14,7 +52,7 @@
 有限な時間(OSのtickなど)で実行することが想定されている。つまり、不定なloop はgoto文の
 外で組み合わされる。
 
-CbC はLLVM/GCC で実装されている。コンパイラの Basic block に相当すると考えてもよい。
+CbC はLLVM\cite{llvm}/GCC\cite{gcc} で実装されている。コンパイラの Basic block に相当すると考えてもよい。
 C form では例えば以下のように記述する。ここでは変数は record Env に格納されている。
 
     __code whileLoop(Env *en, __code next(Env *en)) {