Mercurial > hg > Papers > 2017 > atton-master

comparison presentation/slide.pdf.html @ 115:d731f2d0947d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add Makefile
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Mon, 13 Feb 2017 17:15:10 +0900
parents 5cca315b0230
children ed6719c301fc
comparison
equal deleted inserted replaced
114:5cca315b0230 115:d731f2d0947d
68 68
69 <div class='slide '> 69 <div class='slide '>
70 <!-- === begin markdown block === 70 <!-- === begin markdown block ===
71 71
72 generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16] 72 generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16]
73 on 2017-02-13 16:01:12 +0900 with Markdown engine kramdown (1.13.0) 73 on 2017-02-13 17:14:46 +0900 with Markdown engine kramdown (1.13.0)
74 using options {} 74 using options {}
75 --> 75 -->
76 76
77 <!-- _S9SLIDE_ --> 77 <!-- _S9SLIDE_ -->
78 <h1 id="section">プログラミング言語とソフトウェアの信頼性</h1> 78 <h1 id="section">プログラミング言語とソフトウェアの信頼性</h1>
320 </ul> 320 </ul>
321 </li> 321 </li>
322 <li>ノーマルレベルのコードを検証用に変更せず検証可能</li> 322 <li>ノーマルレベルのコードを検証用に変更せず検証可能</li>
323 </ul> 323 </ul>
324 324
325 <p><img src="./images/akashaPut.svg" alt="akashaPut" width="50%" /></p> 325 <p><img src="./images/akashaPut.svg" alt="akashaPut" width="51%" /></p>
326 326
327 327
328 </div> 328 </div>
329 <div class='slide '> 329 <div class='slide '>
330 <!-- _S9SLIDE_ --> 330 <!-- _S9SLIDE_ -->
459 <!-- _S9SLIDE_ --> 459 <!-- _S9SLIDE_ -->
460 <h1 id="agda-">Agda 上のメタ計算</h1> 460 <h1 id="agda-">Agda 上のメタ計算</h1>
461 <ul> 461 <ul>
462 <li>ノーマルレベルの型を保持したままメタレベルの計算を利用できる 462 <li>ノーマルレベルの型を保持したままメタレベルの計算を利用できる
463 <ul> 463 <ul>
464 <li>cs0 の定義はメタ計算用に変更しなくても良い 464 <li>cs0 の定義はメタ計算用に変更しなくても良い</li>
465 ~~~ 465 </ul>
466 main : ds1 466 </li>
467 </ul>
468
469 <pre><code>main : ds1
467 main = goto cs0 (record {a = 100 ; b = 50}) 470 main = goto cs0 (record {a = 100 ; b = 50})
468 ~~~ 471 </code></pre>
469 ~~~ 472 <pre><code>main : Meta
470 main : Meta 473 main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)})
471 main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c’ = 0 ; next = (N.cs id)}) 474 </code></pre>
472 ~~~</li>
473 </ul>
474 </li>
475 </ul>
476 475
477 476
478 </div> 477 </div>
479 <div class='slide '> 478 <div class='slide '>
480 <!-- _S9SLIDE_ --> 479 <!-- _S9SLIDE_ -->