Mercurial > hg > Papers > 2023 > moririn-sigos

changeset 3:16a733cb4a61

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 17 Apr 2023 18:36:55 +0900
parents 10f239f92691
children 854b01e2ce98
files main.pdf main.tex rbtree.ind
diffstat 3 files changed, 17 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
Binary file main.pdf has changed
--- a/main.tex	Mon Apr 17 11:49:31 2023 +0900
+++ b/main.tex	Mon Apr 17 18:36:55 2023 +0900
@@ -39,9 +39,9 @@
 
 % 和文著者名
 \author{
-{河野真治} \\
+{森　逸汰} {河野真治} \\
 琉球大学工学部\\
-{Shinji KONO} \\
+{Itta Mori} {Shinji KONO} \\
 Faculty of Engineering, University of the Ryukyus\\
 }
 
--- a/rbtree.ind	Mon Apr 17 11:49:31 2023 +0900
+++ b/rbtree.ind	Mon Apr 17 18:36:55 2023 +0900
@@ -1,6 +1,6 @@
 -title: GearsAgdaによる Red Black Tree の検証
 
--author: 河野真治 
+-author: 森逸汰 and 河野真治 
 
 --abstract:
 
@@ -10,20 +10,30 @@
 り、Red Black Treeの検証を行う。並行実行は、Model 検査をGeas
 Agda上で形式化することにより実現する。これについて考察を行う。
 
+--abstract-e:
+
+In GearsAgda, verification of Binary Trees was made possible
+by implementing Hoare Logic on Agda. We want to extend this
+to the verification of RedBlack Trees and concurrent execution
+on these trees. By expanding the invariant, we can verify RedBlack
+Trees. Concurrent execution can be achieved by formalizing 
+Model Checking on GearsAgda. Considerations need to be made
+for this. 
+
 --検証された Red Black Treeの重要性
 
 OSを含むアプリケーションの信頼性は、当然、OSのアプリケーションの両方の信頼性を上げる必要がある。
 信頼性を上げる手法には、テストやモデル検査などがあるが、数学的な証明を行うことが基本である。
 
 最近では、定理証明を高階直観論理あるいは高階関数型言語で行うことができる。これは、Curry Howard
-対応\cite{currey-howard}と呼ばれる命題と型の対応、そして、推論と関数の対応があるためである。実際には、
-Curry Howard 対応が、高階直観論理の意味を決めるのを主導していくことになる。例えば Coq \cite{coq}やIsabel HOL\cite{isabel}
+対応\cite{Girard:1989:PT:64805}と呼ばれる命題と型の対応、そして、推論と関数の対応があるためである。実際には、
+Curry Howard 対応が、高階直観論理の意味を決めるのを主導していくことになる。例えば Coq \cite{Coq}やIsabel HOL\cite{Klein:2014:CFV:2584468.2560537}
 そして、本論文で使用するAgda \cite{agda}が知られている。
 
 一般的なプログラムにはループや再帰呼び出しがあり、メモリや並行実行などと関連している。
 メモリや並行実行あるいはI/Oは、プログラムの関数としての性質とは直接は関係しないので、
 副作用と呼ばれることもある。これらを理論的に扱う手法としてMonadがある。
-Monad \cite{monad} は通常の関数にメタ情報を扱う構造を付加する方法になる。
+Monad \cite{citeulike:6650957,Moggi:1989:CLM:77350.77353} は通常の関数にメタ情報を扱う構造を付加する方法になる。
 
 OSを含むアプリケーションは、証明を意識した手法でプログラミングされるべきであり、
 一つの方法は、すべてをリストのような特定の型変数を含むデータ構造(関手)として
@@ -130,7 +140,7 @@
 証明できる。loop の停止性の証明は、command 対してそれぞれ別に行う必要がある。
 
 この方法では command 毎に Hoare logic のSoundnessを定義する必要がある。実際に Hoare logic をAgdaで実装した
-例がある\cite{}。
+例がある\cite{agda2-hoare}。
 
 --GearsAgda でのプログラム検証手法