changeset 23:973fadbd6687

Mini fixes
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 10 Dec 2014 16:28:34 +0900
parents 743bb64e8f2a
children 158ee14c3615
files sigse.pdf sigse.tex
diffstat 2 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
Binary file sigse.pdf has changed
--- a/sigse.tex	Wed Dec 10 16:23:30 2014 +0900
+++ b/sigse.tex	Wed Dec 10 16:28:34 2014 +0900
@@ -88,7 +88,7 @@
 
 私は研究において関数型プログラミング言語Haskellと証明支援系プログラミング言語Agdaを利用している.
 プログラムの変更を表すことのできるデータ型を用意し,異なるバージョンのプログラム間の関係を形式化する試みである.
-この研究において,Haskell でデータ型と対応する処理を50行ほど記述した.
+この研究において,Haskell でデータ型とそのデータ型への処理を50行ほど記述した.
 そのデータ型と処理が満たすべき条件をAgdaで記述すると500行ほどとなった.
 行換算すると実装に対して仕様には10倍のコストがかかっている.
 Agda では非常に単純な性質は自動で導くが,ほとんどの性質は自ら記述する.
@@ -109,7 +109,7 @@
 対話的に形式手法を実行するためには実行可能プログラムの処理系が形式手法をサポートする必要がある.
 そのためにプログラムに加えるべき情報と制約に興味がある.
 特に,現在は型の情報と制約について調べている.
-私としては情報量は十分だが制約が強すぎるのではないかと考えている.
+私としては依存型は情報量は十分だが制約が強すぎ,線形型では情報量が不十分なのでは無いかと考えている.
 
 %}