Mercurial > hg > Papers > 2018 > ryokka-thesis

--- a/presen/slide.html	Wed Feb 21 13:03:19 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,248 +0,0 @@
-<!DOCTYPE html>
-<html>
-<head>
-   <meta http-equiv="content-type" content="text/html;charset=utf-8">
-   <title>「Agda による継続を用いたプログラムの検証」</title>
-
-<meta name="generator" content="Slide Show (S9) v2.5.0 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin16]">
-<meta name="author"    content="外間 政尊" >
-
-<!-- style sheet links -->
-<link rel="stylesheet" href="s6/themes/projection.css"   media="screen,projection">
-<link rel="stylesheet" href="s6/themes/screen.css"       media="screen">
-<link rel="stylesheet" href="s6/themes/print.css"        media="print">
-<link rel="stylesheet" href="s6/themes/blank.css"        media="screen,projection">
-
-<!-- JS -->
-<script src="s6/js/jquery-1.11.3.min.js"></script>
-<script src="s6/js/jquery.slideshow.js"></script>
-<script src="s6/js/jquery.slideshow.counter.js"></script>
-<script src="s6/js/jquery.slideshow.controls.js"></script>
-<script src="s6/js/jquery.slideshow.footer.js"></script>
-<script src="s6/js/jquery.slideshow.autoplay.js"></script>
-
-<!-- prettify -->
-<link rel="stylesheet" href="scripts/prettify.css">
-<script src="scripts/prettify.js"></script>
-
-<script>
-  $(document).ready( function() {
-    Slideshow.init();
-
-    $('code').each(function(_, el) {
-      if (!el.classList.contains('noprettyprint')) {
-        el.classList.add('prettyprint');
-      }
-    });
-    prettyPrint();
-  } );
-
-
-</script>
-
-<!-- Better Browser Banner for Microsoft Internet Explorer (IE) -->
-<!--[if IE]>
-<script src="s6/js/jquery.microsoft.js"></script>
-<![endif]-->
-
-
-
-</head>
-<body>
-
-<div class="layout">
-  <div id="header"></div>
-  <div id="footer">
-    <div align="right">
-      <img src="s6/images/logo.svg" width="200px">
-    </div>
-  </div>
-</div>
-
-<div class="presentation">
-
-  <div class='slide cover'>
-    <table width="90%" height="90%" border="0" align="center">
-      <tr>
-        <td>
-          <div align="center">
-            <h1><font color="#808db5">「Agda による継続を用いたプログラムの検証」</font></h1>
-          </div>
-        </td>
-      </tr>
-      <tr>
-        <td>
-          <div align="left">
-            外間 政尊
-            @並列信頼研
-            <hr style="color:#ffcc00;background-color:#ffcc00;text-align:left;border:none;width:100%;height:0.2em;">
-          </div>
-        </td>
-      </tr>
-    </table>
-  </div>
-
-<div class='slide '>
-<!-- === begin markdown block ===
-
-      generated by markdown/1.2.0 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin16]
-                on 2018-02-19 03:03:45 +0900 with Markdown engine kramdown (1.15.0)
-                  using options {}
-  -->
-
-<!-- _S9SLIDE_ -->
-<h1 id="section">研究概要</h1>
-
-<ul>
-  <li>
-    <p>動作するプログラムの信頼性を保証したい</p>
-  </li>
-  <li>
-    <p>そのために当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している</p>
-  </li>
-  <li>
-    <p>処理の単位である CodeGear はメタ計算によって接続され、メタ計算部分を切り替えることで CodeGear に一切の変更なくプログラムの性質を検証することができる</p>
-  </li>
-  <li>
-    <p>本研究では CodeGear 、 DataGear を用いて記述する言語、 Continuation based C (CbC) を用いてプログラムを記述し、それを証明することで信頼性を上げることを目標としている</p>
-  </li>
-  <li>
-    <p>CbC での記述を Agda にマッピングし、その性質の一部を証明した</p>
-  </li>
-</ul>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h1 id="codegear--datagear">CodeGear と DataGear</h1>
-
-<ul>
-  <li>
-    <p>CodeGear とはプログラムを記述する際の処理の単位である。</p>
-  </li>
-  <li>
-    <p>DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている。</p>
-  </li>
-  <li>
-    <p>CodeGear はメタ計算によって CodeGear へ接続される</p>
-  </li>
-  <li>
-    <p>CodeGear は入力として DataGear を受け取り、 DataGear に変更を加えて次に指定された CodeGear へ継続する。</p>
-  </li>
-</ul>
-
-<!-- CbC のスライドを作って間にいれる…？ -->
-<p># Continuation based C (CbC)</p>
-
-<ul>
-  <li>
-    <p>当研究室で開発している言語</p>
-  </li>
-  <li>
-    <p>基本的な構文は C lang</p>
-  </li>
-  <li>
-    <p>前述の CodeGear DataGear を用いてプログラムを記述する</p>
-  </li>
-  <li>
-    <p>CodeGear を継続し、 DataGear を変更しながらプログラムが進んでいく</p>
-  </li>
-  <li>
-    <p>DataGear をCodeGearで扱う際に、直接触れるといろいろできちゃう</p>
-  </li>
-  <li>
-    <p>その為、 Context というものを通して CodeGear の メタ計算として stub CodeGear を通して Context からデータを取ってきて変更して DataGear に返すということをしている。</p>
-  </li>
-  <li>
-    <p>現段階で複雑でない stub CodeGear はスクリプトを使って自動生成している</p>
-  </li>
-  <li>
-    <p>ただ、複雑な処理をする際には stub CodeGear を手動で書く必要がある、煩雑。</p>
-  </li>
-</ul>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h1 id="interface">Interface</h1>
-
-<ul>
-  <li>
-    <p>そこで Interface を記述することになった</p>
-  </li>
-  <li>
-    <p>データ構造としての api と DataGear を結びつけて呼び出しやすくなった</p>
-  </li>
-</ul>
-
-<!-- interface の例 -->
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h1 id="agda">Agda</h1>
-
-<ul>
-  <li>
-    <p>Agda とは定理証明支援器で、型システムを用いて証明を記述できる。</p>
-  </li>
-  <li>
-    <p>Agda 上でも CodeGear、 DataGear の単位と継続を定義した(「メタ計算を用いた Continuation based C」琉球大学工学部情報工学科平成 29 年度学位論文(修士)より)</p>
-  </li>
-  <li>
-    <p>Agda上でも CbC の Interface と同様のものを記述した。</p>
-  </li>
-</ul>
-
-<!-- AgdaのInterface の例 -->
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h1 id="agda--interface-stack-">Agda での Interface の部分的な証明(Stack の例)</h1>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h1 id="agda--interface-tree-">Agda での Interface の部分的な証明(Tree の例)</h1>
-
-<!-- なんでだめなのかがうまく説明できないかも… -->
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h1 id="hoare-logic">Hoare Logic</h1>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h1 id="section-1">今後の課題</h1>
-
-<ul>
-  <li>
-    <p>本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。</p>
-  </li>
-  <li>
-    <p>これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。</p>
-  </li>
-  <li>
-    <p>また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。</p>
-  </li>
-  <li>
-    <p>今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。</p>
-  </li>
-</ul>
-<!-- === end markdown block === -->
-</div>
-
-
-</div><!-- presentation -->
-</body>
-</html>
--- a/presen/slide.md	Wed Feb 21 13:03:19 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,89 +0,0 @@
-title: 「Agda による継続を用いたプログラムの検証」
-author: 外間 政尊
-profile: @並列信頼研
-lang: Japanese
-code-engine: coderay
-
-
-# 研究概要
-
-* 動作するプログラムの信頼性を保証したい
-
-* そのために当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している
-
-* 処理の単位である CodeGear はメタ計算によって接続され、メタ計算部分を切り替えることで CodeGear に一切の変更なくプログラムの性質を検証することができる
-
-* 本研究では CodeGear 、 DataGear を用いて記述する言語、 Continuation based C (CbC) を用いてプログラムを記述し、それを証明することで信頼性を上げることを目標としている
-
-* CbC での記述を Agda にマッピングし、その性質の一部を証明した
-
-# CodeGear と DataGear
-
-* CodeGear とはプログラムを記述する際の処理の単位である。
-
-* DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている。
-
-* CodeGear はメタ計算によって CodeGear へ接続される
-
-* CodeGear は入力として DataGear を受け取り、 DataGear に変更を加えて次に指定された CodeGear へ継続する。
-
-
-<!-- CbC のスライドを作って間にいれる…？ -->
-# Continuation based C (CbC)
-
-* 当研究室で開発している言語
-
-* 基本的な構文は C lang
-
-* 前述の CodeGear DataGear を用いてプログラムを記述する
-
-* CodeGear を継続し、 DataGear を変更しながらプログラムが進んでいく
-
-* DataGear をCodeGearで扱う際に、直接触れるといろいろできちゃう
-
-* その為、 Context というものを通して CodeGear の メタ計算として stub CodeGear を通して Context からデータを取ってきて変更して DataGear に返すということをしている。
-
-* 現段階で複雑でない stub CodeGear はスクリプトを使って自動生成している
-
-* ただ、複雑な処理をする際には stub CodeGear を手動で書く必要がある、煩雑。
-
-# Interface
-
-* そこで Interface を記述することになった
-
-* データ構造としての api と DataGear を結びつけて呼び出しやすくなった
-
-<!-- interface の例 -->
-
-# Agda
-
-* Agda とは定理証明支援器で、型システムを用いて証明を記述できる。
-
-* Agda 上でも CodeGear、 DataGear の単位と継続を定義した(「メタ計算を用いた Continuation based C」琉球大学工学部情報工学科平成 29 年度学位論文(修士)より)
-
-* Agda上でも CbC の Interface と同様のものを記述した。
-
-<!-- AgdaのInterface の例 -->
-
-# Agda での Interface の部分的な証明(Stack の例)
-
-
-
-# Agda での Interface の部分的な証明(Tree の例)
-
-<!-- なんでだめなのかがうまく説明できないかも… -->
-
-
-# Hoare Logic
-
-
-
-# 今後の課題
-
-* 本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。
-
-* これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。
-
-* また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。
-
-* 今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。