Mercurial > hg > Papers > 2018 > ryokka-thesis
comparison thesis.mm @ 1:0035f6d4826f
fix MindMap,add some chapter
author | ryokka |
---|---|
date | Thu, 01 Feb 2018 01:14:30 +0900 |
parents | 46d543c569d2 |
children | 2155c6ff589f |
comparison
equal
deleted
inserted
replaced
0:46d543c569d2 | 1:0035f6d4826f |
---|---|
1 <map version="1.1.0"> | 1 <map version="1.1.0"> |
2 <!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net --> | 2 <!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net --> |
3 <node CREATED="1516447600591" ID="ID_1323189017" MODIFIED="1516447624027" TEXT="thesis"> | 3 <node CREATED="1516447600591" ID="ID_1323189017" MODIFIED="1516447624027" TEXT="thesis"> |
4 <node CREATED="1516447625087" ID="ID_1724518003" MODIFIED="1516447637346" POSITION="left" TEXT="はじめに"> | 4 <node CREATED="1516447625087" FOLDED="true" ID="ID_1724518003" MODIFIED="1517385478036" POSITION="left" TEXT="はじめに"> |
5 <node CREATED="1516448006125" ID="ID_801881892" MODIFIED="1516448107906" TEXT="動作するプログラムの信頼性を保証したい"/> | 5 <node CREATED="1516448006125" ID="ID_801881892" MODIFIED="1516448107906" TEXT="動作するプログラムの信頼性を保証したい"/> |
6 <node CREATED="1516448247561" ID="ID_951851740" MODIFIED="1516448282443" TEXT="CodeSegment,DataSegmentという単位でプログラムを書く手法を提案している"/> | 6 <node CREATED="1516448247561" ID="ID_951851740" MODIFIED="1516448282443" TEXT="CodeSegment,DataSegmentという単位でプログラムを書く手法を提案している"/> |
7 <node CREATED="1516448220906" ID="ID_182832086" MODIFIED="1516448412313" TEXT="CbC(Continuation based C )ではこのようにプログラムを記述することでメタ計算として検証をすることができた(あっとんさんの論文)"/> | 7 <node CREATED="1516448220906" ID="ID_182832086" MODIFIED="1516448412313" TEXT="CbC(Continuation based C )ではこのようにプログラムを記述することでメタ計算として検証をすることができた(あっとんさんの論文)"/> |
8 <node CREATED="1516448414254" ID="ID_1047962267" MODIFIED="1516448573215" TEXT="CbCでは自身で証明をすることができない為、(何らかの理由で)Agdaを使って証明する"/> | 8 <node CREATED="1516448414254" ID="ID_1047962267" MODIFIED="1516448573215" TEXT="CbCでは自身で証明をすることができない為、(何らかの理由で)Agdaを使って証明する"/> |
9 <node CREATED="1516448574477" ID="ID_1442131681" MODIFIED="1516453035591" TEXT="本研究ではAgdaでCodeSegment、DataSegmentという単位を使ってCbCで記述したものと等価なUnbarrancedTreeを作り、ノードを入れる際ノードがなくならないこと、などを証明をする"/> | 9 <node CREATED="1516448574477" ID="ID_1442131681" MODIFIED="1516453035591" TEXT="本研究ではAgdaでCodeSegment、DataSegmentという単位を使ってCbCで記述したものと等価なUnbarrancedTreeを作り、ノードを入れる際ノードがなくならないこと、などを証明をする"/> |
10 </node> | 10 </node> |
11 <node CREATED="1516447638226" ID="ID_1889545574" MODIFIED="1516448672959" POSITION="left" TEXT="基礎概念"> | 11 <node CREATED="1516447638226" FOLDED="true" ID="ID_1889545574" MODIFIED="1517385480087" POSITION="left" TEXT="基礎概念"> |
12 <node CREATED="1516448673422" ID="ID_1274177968" MODIFIED="1516448683325" TEXT="CbC"> | 12 <node CREATED="1516448673422" ID="ID_1274177968" MODIFIED="1516448683325" TEXT="CbC"> |
13 <node CREATED="1516448708973" ID="ID_815925469" MODIFIED="1516454414422" TEXT="CodeSegmentとは"> | 13 <node CREATED="1516448708973" ID="ID_815925469" MODIFIED="1516454414422" TEXT="CodeSegmentとは"> |
14 <node CREATED="1516454422237" ID="ID_661052887" MODIFIED="1516454424583" TEXT="例題"/> | 14 <node CREATED="1516454422237" ID="ID_661052887" MODIFIED="1516454424583" TEXT="例題"/> |
15 </node> | 15 </node> |
16 <node CREATED="1516448719701" ID="ID_1017753652" MODIFIED="1516454421110" TEXT="DataSegmentとは"> | 16 <node CREATED="1516448719701" ID="ID_1017753652" MODIFIED="1516454421110" TEXT="DataSegmentとは"> |
17 <node CREATED="1516454425392" ID="ID_221829180" MODIFIED="1516454427407" TEXT="例題"/> | 17 <node CREATED="1516454425392" ID="ID_221829180" MODIFIED="1516454427407" TEXT="例題"/> |
18 </node> | 18 </node> |
19 <node CREATED="1517214307007" ID="ID_1524511628" MODIFIED="1517214330536" TEXT="Metaな話は多分いらない"/> | |
19 </node> | 20 </node> |
20 <node CREATED="1516448688109" ID="ID_594761054" MODIFIED="1516448692742" TEXT="証明"> | 21 <node CREATED="1516448684110" ID="ID_1770419109" MODIFIED="1517214374341" TEXT="Agda"> |
21 <node CREATED="1516454132267" ID="ID_1490526606" MODIFIED="1516693045587" TEXT="自然証明"> | |
22 <node CREATED="1516454431900" ID="ID_1113949900" MODIFIED="1516454434111" TEXT="例題"/> | |
23 </node> | |
24 <node CREATED="1516454140637" ID="ID_1834687592" MODIFIED="1516455188550" TEXT="カリーハワード同型対応"/> | |
25 </node> | |
26 <node CREATED="1516448684110" ID="ID_1770419109" MODIFIED="1516448687493" TEXT="Agda"> | |
27 <node CREATED="1516454190133" ID="ID_445682748" MODIFIED="1516454207271" TEXT="その他の証明支援系"/> | 22 <node CREATED="1516454190133" ID="ID_445682748" MODIFIED="1516454207271" TEXT="その他の証明支援系"/> |
28 <node CREATED="1516454167956" ID="ID_1326840818" MODIFIED="1516454171204" TEXT="記述方法"/> | 23 <node CREATED="1516454167956" ID="ID_1326840818" MODIFIED="1516454171204" TEXT="記述方法"/> |
29 <node CREATED="1516454171715" ID="ID_1880237124" MODIFIED="1516454184781" TEXT="例題"/> | 24 <node CREATED="1516454171715" ID="ID_1880237124" MODIFIED="1516454184781" TEXT="例題"/> |
30 </node> | 25 </node> |
26 <node CREATED="1516448688109" ID="ID_594761054" MODIFIED="1516448692742" TEXT="証明"> | |
27 <node CREATED="1516454132267" ID="ID_1490526606" MODIFIED="1516693045587" TEXT="自然証明"> | |
28 <node CREATED="1517214338214" ID="ID_794688351" MODIFIED="1517214354528" TEXT="説明"/> | |
29 <node CREATED="1516454431900" ID="ID_1113949900" MODIFIED="1516454434111" TEXT="例題"/> | |
30 </node> | |
31 <node CREATED="1516454140637" ID="ID_1834687592" MODIFIED="1516455188550" TEXT="カリーハワード同型対応"/> | |
32 <node CREATED="1517214363342" ID="ID_1381920910" MODIFIED="1517214367584" TEXT="Agdaでの証明"/> | |
33 </node> | |
31 <node CREATED="1516448778576" ID="ID_1454457815" MODIFIED="1516453085568" TEXT="Tree,RedBlackTree"/> | 34 <node CREATED="1516448778576" ID="ID_1454457815" MODIFIED="1516453085568" TEXT="Tree,RedBlackTree"/> |
32 </node> | 35 </node> |
33 <node CREATED="1516448781436" ID="ID_732614714" MODIFIED="1516448784603" POSITION="left" TEXT="実験"> | 36 <node CREATED="1516448781436" FOLDED="true" ID="ID_732614714" MODIFIED="1517385481609" POSITION="left" TEXT="実験"> |
34 <node CREATED="1516448792793" ID="ID_590034820" MODIFIED="1516448919993" TEXT="Treeの作成方針"/> | 37 <node CREATED="1516448792793" ID="ID_590034820" MODIFIED="1516448919993" TEXT="Treeの作成方針"/> |
35 <node CREATED="1516448843266" ID="ID_1177321611" MODIFIED="1516454291651" TEXT="証明方針の検討,実装時の改善"/> | 38 <node CREATED="1516448843266" ID="ID_1177321611" MODIFIED="1516454291651" TEXT="証明方針の検討,実装時の改善"/> |
36 </node> | 39 </node> |
37 <node CREATED="1516448766134" ID="ID_712304841" MODIFIED="1516448768937" POSITION="left" TEXT="実装"> | 40 <node CREATED="1516448766134" FOLDED="true" ID="ID_712304841" MODIFIED="1517385482976" POSITION="left" TEXT="実装"> |
38 <node CREATED="1516448769994" ID="ID_1122278060" MODIFIED="1516453267632" TEXT="CbCでの実装"/> | 41 <node CREATED="1516448769994" ID="ID_1122278060" MODIFIED="1516453267632" TEXT="CbCでの実装"/> |
39 <node CREATED="1516453268445" ID="ID_1239636691" MODIFIED="1516453272713" TEXT="Agdaでの実装"/> | 42 <node CREATED="1516453268445" ID="ID_1239636691" MODIFIED="1516453272713" TEXT="Agdaでの実装"/> |
40 <node CREATED="1516453273168" ID="ID_1420286449" MODIFIED="1516454130460" TEXT="Agdaでの証明,解説"/> | 43 <node CREATED="1516453273168" ID="ID_1420286449" MODIFIED="1516454130460" TEXT="Agdaでの証明,解説"/> |
41 </node> | 44 </node> |
42 <node CREATED="1516455668900" ID="ID_155403381" MODIFIED="1516455671387" POSITION="left" TEXT="評価"> | 45 <node CREATED="1516455668900" FOLDED="true" ID="ID_155403381" MODIFIED="1517385484966" POSITION="left" TEXT="評価"> |
43 <node CREATED="1516455671828" ID="ID_1828774278" MODIFIED="1516455677370" TEXT="?"/> | 46 <node CREATED="1516455671828" ID="ID_1828774278" MODIFIED="1516455677370" TEXT="?"/> |
44 </node> | 47 </node> |
45 <node CREATED="1516448787093" ID="ID_1477806830" MODIFIED="1516448789500" POSITION="left" TEXT="結論"> | 48 <node CREATED="1516448787093" FOLDED="true" ID="ID_1477806830" MODIFIED="1517385486194" POSITION="left" TEXT="結論"> |
46 <node CREATED="1516453116787" ID="ID_1750859738" MODIFIED="1516453146188" TEXT="TreeをCodeSegment,DataSegmentを用いて二つの言語で記述した"/> | 49 <node CREATED="1516453116787" ID="ID_1750859738" MODIFIED="1516453146188" TEXT="TreeをCodeSegment,DataSegmentを用いて二つの言語で記述した"/> |
47 <node CREATED="1516453146841" ID="ID_495843685" MODIFIED="1516695852072" TEXT="等価なコードができた?"/> | 50 <node CREATED="1516453146841" ID="ID_495843685" MODIFIED="1516695852072" TEXT="等価なコードができた?"/> |
48 <node CREATED="1516453179338" ID="ID_710713278" MODIFIED="1516695815136" TEXT="証明支援器を使ってunBalanceなTreeができることを証明した?"/> | 51 <node CREATED="1516453179338" ID="ID_710713278" MODIFIED="1516695815136" TEXT="証明支援器を使ってunBalanceなTreeができることを証明した?"/> |
49 <node CREATED="1516693502350" ID="ID_1803347987" MODIFIED="1516695887153" TEXT="その他、今後の話"> | 52 <node CREATED="1516693502350" ID="ID_1803347987" MODIFIED="1516695887153" TEXT="その他、今後の話"> |
50 <node CREATED="1516693505485" ID="ID_727445874" MODIFIED="1516693962403" TEXT="CbCのコンパイル時にTypeCheckingもできるかもしれないねみたいなはなし"/> | 53 <node CREATED="1516693505485" ID="ID_727445874" MODIFIED="1516693962403" TEXT="CbCのコンパイル時にTypeCheckingもできるかもしれないねみたいなはなし"/> |
51 </node> | 54 </node> |
52 </node> | 55 </node> |
53 <node CREATED="1516695662563" ID="ID_1054440656" MODIFIED="1516695667362" POSITION="right" TEXT="章構成"> | 56 <node CREATED="1516695662563" ID="ID_1054440656" MODIFIED="1516695667362" POSITION="right" TEXT="章構成"> |
54 <node CREATED="1516695644106" ID="ID_736329900" MODIFIED="1516695909066" TEXT="研究背景"/> | 57 <node CREATED="1516695644106" ID="ID_736329900" MODIFIED="1516695909066" TEXT="研究背景"> |
55 <node CREATED="1516695675644" ID="ID_922716453" MODIFIED="1516695971900" TEXT="CbC"/> | 58 <node CREATED="1517385504371" ID="ID_201034437" MODIFIED="1517385507130" TEXT="はじめに"/> |
56 <node CREATED="1516695693068" ID="ID_1567452235" MODIFIED="1516695739269" TEXT="証明とプログラミング"/> | 59 </node> |
57 <node CREATED="1516695699548" ID="ID_1160729877" MODIFIED="1516695701947" TEXT="Agda"/> | 60 <node CREATED="1517384887536" ID="ID_1535504778" MODIFIED="1517384893658" TEXT="CbC"> |
58 <node CREATED="1516695711821" ID="ID_886806884" MODIFIED="1516695769605" TEXT="CbCとAgda"/> | 61 <node CREATED="1516695675644" ID="ID_922716453" MODIFIED="1517385660735" TEXT="CodeSegmentとDataSegment"/> |
59 <node CREATED="1516695770479" ID="ID_289839920" MODIFIED="1516695935530" TEXT="Agdaでの証明"/> | 62 <node CREATED="1517385681042" ID="ID_1583563260" MODIFIED="1517385703041" TEXT="CbCの記述"> |
60 <node CREATED="1516695962331" ID="ID_1727743322" MODIFIED="1516695964397" TEXT="まとめ"/> | 63 <node CREATED="1517385703503" ID="ID_298253554" MODIFIED="1517385713098" TEXT="CbC上でのCodeSegmentの例"/> |
64 <node CREATED="1517385714282" ID="ID_87445580" MODIFIED="1517385732747" TEXT="CbC上でのDataSegmentの例"/> | |
65 </node> | |
66 </node> | |
67 <node CREATED="1516695699548" ID="ID_1160729877" MODIFIED="1517384881720" TEXT="Agda"> | |
68 <node CREATED="1517385743439" ID="ID_948325222" MODIFIED="1517385763996" TEXT="Agda文法"/> | |
69 <node CREATED="1516695675644" ID="ID_1174205441" MODIFIED="1517385787006" TEXT="Agda での CodeSegment、DataSegmentの例"/> | |
70 <node CREATED="1516695711821" ID="ID_886806884" MODIFIED="1517385815751" TEXT="Agda でのInterface部分の例"/> | |
71 </node> | |
72 <node CREATED="1516695693068" ID="ID_1567452235" MODIFIED="1517214279808" TEXT="証明とプログラミング"> | |
73 <node CREATED="1517385849109" ID="ID_808144723" MODIFIED="1517385854297" TEXT="自然演繹"/> | |
74 <node CREATED="1517385855121" ID="ID_910986235" MODIFIED="1517385874635" TEXT="Curry-Howard同型対応"/> | |
75 <node CREATED="1517385877162" ID="ID_869768510" MODIFIED="1517385926540" TEXT="Agdaと自然演繹の証明の例(たぶん三段論法になる?)"/> | |
76 </node> | |
77 <node CREATED="1516695770479" ID="ID_289839920" MODIFIED="1517214287535" TEXT="Agdaでの証明"> | |
78 <node CREATED="1517385826823" ID="ID_778238289" MODIFIED="1517385842945" TEXT="Interface部分の証明(stack,tree)"/> | |
79 </node> | |
80 <node CREATED="1516695962331" ID="ID_1727743322" MODIFIED="1516695964397" TEXT="まとめ"> | |
81 <node CREATED="1517384473095" ID="ID_1131464081" MODIFIED="1517385933785" TEXT="いいたいとこ"> | |
82 <node CREATED="1517384520003" ID="ID_1024027966" MODIFIED="1517384562444" TEXT="Agdaで記述することでGearsの文法的曖昧な部分が明確化された"/> | |
83 <node CREATED="1517384563497" ID="ID_1552767038" MODIFIED="1517384599221" TEXT="先行研究との違い"> | |
84 <node CREATED="1517384599498" ID="ID_7745421" MODIFIED="1517384649848" TEXT="ノーマルレベルでのインターフェース部分の記述"/> | |
85 <node CREATED="1517384690992" ID="ID_895803544" MODIFIED="1517384717943" TEXT="インターフェースを使って抽象化した(stack,tree))"/> | |
86 <node CREATED="1517384651337" ID="ID_1071842343" MODIFIED="1517384658640" TEXT="インターフェース部分の証明"/> | |
87 </node> | |
88 </node> | |
89 </node> | |
61 </node> | 90 </node> |
62 </node> | 91 </node> |
63 </map> | 92 </map> |