Mercurial > hg > Members > atton > generated_seminar_slides

--- a/slides/20160503/slide.html	Tue May 03 17:58:25 2016 +0900
+++ b/slides/20160503/slide.html	Tue May 03 18:00:18 2016 +0900
@@ -2,10 +2,10 @@
 <html>
 <head>
    <meta http-equiv="content-type" content="text/html;charset=utf-8">
-   <title><%= @headers['title'] %></title>
+   <title>Verification of programs using Continuation based C</title>

-<meta name="generator" content="<%= @headers['generator'] %>">
-<meta name="author"    content="<%= @headers['author']%>" >
+<meta name="generator" content="Slide Show (S9) v2.5.0 on Ruby 2.3.0 (2015-12-25) [x86_64-darwin14]">
+<meta name="author"    content="Yasutaka Higa" >

 <!-- style sheet links -->
 <link rel="stylesheet" href="s6/themes/projection.css"   media="screen,projection">
@@ -38,7 +38,7 @@
     prettyPrint();
   } );

-  <%= content_for :js %>
+
 </script>

 <!-- Better Browser Banner for Microsoft Internet Explorer (IE) -->
@@ -46,7 +46,7 @@
 <script src="s6/js/jquery.microsoft.js"></script>
 <![endif]-->

-<%= content_for :head %>
+

 </head>
 <body>
@@ -67,15 +67,15 @@
       <tr>
         <td>
           <div align="center">
-            <h1><font color="#808db5"><%= @headers['title'] %></font></h1>
+            <h1><font color="#808db5">Verification of programs using Continuation based C</font></h1>
           </div>
         </td>
       </tr>
       <tr>
         <td>
           <div align="left">
-            <%= @headers['author'] %>
-            <%= @headers['profile'] %>
+            Yasutaka Higa
+
             <hr style="color:#ffcc00;background-color:#ffcc00;text-align:left;border:none;width:100%;height:0.2em;">
           </div>
         </td>
@@ -83,7 +83,102 @@
     </table>
   </div>

-<%= @content %>
+<div class='slide '>
+<!-- === begin markdown block ===
+
+      generated by markdown/1.2.0 on Ruby 2.3.0 (2015-12-25) [x86_64-darwin14]
+                on 2016-05-03 18:00:09 +0900 with Markdown engine kramdown (1.9.0)
+                  using options {}
+  -->
+
+<!-- _S9SLIDE_ -->
+<h1 id="section">研究目的</h1>
+<ul>
+  <li>コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する</li>
+  <li>プログラムはコードセグメントという処理の集合として表され、相互に接続される</li>
+  <li>個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="section-1">研究内容</h1>
+<ul>
+  <li>コードセグメントとデータセグメントを用いたプログラムに対し、検証を行なう</li>
+  <li>コードセグメントどうしの接続の間にメタ計算として検証機構を導入する</li>
+  <li>コードを検証用に変更することなく、仕様を満たすか検証する</li>
+  <li>検証の対象として Gears OS のデータ構造を用いる</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="section-2">近況報告</h1>
+<ul>
+  <li>SWoPP のネタ
+    <ul>
+      <li>Gears のデータ構造の検証</li>
+      <li>Operational Semantics of CbC</li>
+    </ul>
+  </li>
+  <li>発表申込締切が 2016/05/13 あたりなので来週くらいに発表アブストを持ってきます</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="gears-">Gears のデータ構造の検証</h1>
+<ul>
+  <li>Red-Black Tree
+    <ul>
+      <li>insertion の全探索は13要素までOK</li>
+      <li>6,227,020,800 通り</li>
+    </ul>
+  </li>
+  <li>Synchronized Queue
+    <ul>
+      <li>bounded queue
+        <ul>
+          <li>各 thread が取りえる操作を全探索</li>
+        </ul>
+      </li>
+      <li>unbounded queue
+        <ul>
+          <li>アイデア: 0, 1, 2 以上で抽象化</li>
+        </ul>
+      </li>
+    </ul>
+  </li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="operational-semantics-of-cbc">Operational Semantics of CbC</h1>
+<ul>
+  <li>Agda で CbC を書けるか</li>
+  <li>memory allocation 部分とかは meta に押しつけて書く
+    <ul>
+      <li>待ちあわせとかも無い</li>
+    </ul>
+  </li>
+  <li>cs は ds -&gt; ds
+    <ul>
+      <li>それだと行き先情報が無いので</li>
+      <li>ds に next を含める or State Monad 辺りでやってみる</li>
+    </ul>
+  </li>
+  <li>Agda を 2.5.1 に上げて State Monad を書いてみてます</li>
+</ul>
+
+<!-- vim: set filetype=markdown.slide: -->
+<!-- === end markdown block === -->
+</div>
+

 </div><!-- presentation -->
 </body>