Mercurial > hg > Papers > 2018 > ryokka-sigos

view thesis.mm @ 4:d273fa70e9f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix document
author ryokka
date Sun, 22 Apr 2018 18:42:34 +0900
parents a5facba1adbc
children
line wrap: on
line source

<map version="1.1.0">
<!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net -->
<node CREATED="1516447600591" ID="ID_1323189017" MODIFIED="1516447624027" TEXT="thesis">
<node CREATED="1516447625087" FOLDED="true" ID="ID_1724518003" MODIFIED="1517385478036" POSITION="left" TEXT="&#x306f;&#x3058;&#x3081;&#x306b;">
<node CREATED="1516448006125" ID="ID_801881892" MODIFIED="1516448107906" TEXT="&#x52d5;&#x4f5c;&#x3059;&#x308b;&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30e0;&#x306e;&#x4fe1;&#x983c;&#x6027;&#x3092;&#x4fdd;&#x8a3c;&#x3057;&#x305f;&#x3044;"/>
<node CREATED="1516448247561" ID="ID_951851740" MODIFIED="1516448282443" TEXT="CodeSegment,DataSegment&#x3068;&#x3044;&#x3046;&#x5358;&#x4f4d;&#x3067;&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30e0;&#x3092;&#x66f8;&#x304f;&#x624b;&#x6cd5;&#x3092;&#x63d0;&#x6848;&#x3057;&#x3066;&#x3044;&#x308b;"/>
<node CREATED="1516448220906" ID="ID_182832086" MODIFIED="1516448412313" TEXT="CbC(Continuation  based C )&#x3067;&#x306f;&#x3053;&#x306e;&#x3088;&#x3046;&#x306b;&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30e0;&#x3092;&#x8a18;&#x8ff0;&#x3059;&#x308b;&#x3053;&#x3068;&#x3067;&#x30e1;&#x30bf;&#x8a08;&#x7b97;&#x3068;&#x3057;&#x3066;&#x691c;&#x8a3c;&#x3092;&#x3059;&#x308b;&#x3053;&#x3068;&#x304c;&#x3067;&#x304d;&#x305f;&#xff08;&#x3042;&#x3063;&#x3068;&#x3093;&#x3055;&#x3093;&#x306e;&#x8ad6;&#x6587;&#xff09;"/>
<node CREATED="1516448414254" ID="ID_1047962267" MODIFIED="1516448573215" TEXT="CbC&#x3067;&#x306f;&#x81ea;&#x8eab;&#x3067;&#x8a3c;&#x660e;&#x3092;&#x3059;&#x308b;&#x3053;&#x3068;&#x304c;&#x3067;&#x304d;&#x306a;&#x3044;&#x70ba;&#x3001;&#xff08;&#x4f55;&#x3089;&#x304b;&#x306e;&#x7406;&#x7531;&#x3067;&#xff09;Agda&#x3092;&#x4f7f;&#x3063;&#x3066;&#x8a3c;&#x660e;&#x3059;&#x308b;"/>
<node CREATED="1516448574477" ID="ID_1442131681" MODIFIED="1516453035591" TEXT="&#x672c;&#x7814;&#x7a76;&#x3067;&#x306f;Agda&#x3067;CodeSegment&#x3001;DataSegment&#x3068;&#x3044;&#x3046;&#x5358;&#x4f4d;&#x3092;&#x4f7f;&#x3063;&#x3066;CbC&#x3067;&#x8a18;&#x8ff0;&#x3057;&#x305f;&#x3082;&#x306e;&#x3068;&#x7b49;&#x4fa1;&#x306a;UnbarrancedTree&#x3092;&#x4f5c;&#x308a;&#x3001;&#x30ce;&#x30fc;&#x30c9;&#x3092;&#x5165;&#x308c;&#x308b;&#x969b;&#x30ce;&#x30fc;&#x30c9;&#x304c;&#x306a;&#x304f;&#x306a;&#x3089;&#x306a;&#x3044;&#x3053;&#x3068;&#x3001;&#x306a;&#x3069;&#x3092;&#x8a3c;&#x660e;&#x3092;&#x3059;&#x308b;"/>
</node>
<node CREATED="1516447638226" FOLDED="true" ID="ID_1889545574" MODIFIED="1517919048296" POSITION="left" TEXT="&#x57fa;&#x790e;&#x6982;&#x5ff5;">
<node CREATED="1516448673422" ID="ID_1274177968" MODIFIED="1516448683325" TEXT="CbC">
<node CREATED="1516448708973" ID="ID_815925469" MODIFIED="1516454414422" TEXT="CodeSegment&#x3068;&#x306f;">
<node CREATED="1516454422237" ID="ID_661052887" MODIFIED="1516454424583" TEXT="&#x4f8b;&#x984c;"/>
</node>
<node CREATED="1516448719701" ID="ID_1017753652" MODIFIED="1516454421110" TEXT="DataSegment&#x3068;&#x306f;">
<node CREATED="1516454425392" ID="ID_221829180" MODIFIED="1516454427407" TEXT="&#x4f8b;&#x984c;"/>
</node>
<node CREATED="1517214307007" ID="ID_1524511628" MODIFIED="1517214330536" TEXT="Meta&#x306a;&#x8a71;&#x306f;&#x591a;&#x5206;&#x3044;&#x3089;&#x306a;&#x3044;"/>
</node>
<node CREATED="1516448684110" ID="ID_1770419109" MODIFIED="1517214374341" TEXT="Agda">
<node CREATED="1516454190133" ID="ID_445682748" MODIFIED="1516454207271" TEXT="&#x305d;&#x306e;&#x4ed6;&#x306e;&#x8a3c;&#x660e;&#x652f;&#x63f4;&#x7cfb;"/>
<node CREATED="1516454167956" ID="ID_1326840818" MODIFIED="1516454171204" TEXT="&#x8a18;&#x8ff0;&#x65b9;&#x6cd5;"/>
<node CREATED="1516454171715" ID="ID_1880237124" MODIFIED="1516454184781" TEXT="&#x4f8b;&#x984c;"/>
</node>
<node CREATED="1516448688109" ID="ID_594761054" MODIFIED="1516448692742" TEXT="&#x8a3c;&#x660e;">
<node CREATED="1516454132267" ID="ID_1490526606" MODIFIED="1516693045587" TEXT="&#x81ea;&#x7136;&#x8a3c;&#x660e;">
<node CREATED="1517214338214" ID="ID_794688351" MODIFIED="1517214354528" TEXT="&#x8aac;&#x660e;"/>
<node CREATED="1516454431900" ID="ID_1113949900" MODIFIED="1516454434111" TEXT="&#x4f8b;&#x984c;"/>
</node>
<node CREATED="1516454140637" ID="ID_1834687592" MODIFIED="1516455188550" TEXT="&#x30ab;&#x30ea;&#x30fc;&#x30cf;&#x30ef;&#x30fc;&#x30c9;&#x540c;&#x578b;&#x5bfe;&#x5fdc;"/>
<node CREATED="1517214363342" ID="ID_1381920910" MODIFIED="1517214367584" TEXT="Agda&#x3067;&#x306e;&#x8a3c;&#x660e;"/>
</node>
<node CREATED="1516448778576" ID="ID_1454457815" MODIFIED="1516453085568" TEXT="Tree,RedBlackTree"/>
</node>
<node CREATED="1516448781436" FOLDED="true" ID="ID_732614714" MODIFIED="1517385481609" POSITION="left" TEXT="&#x5b9f;&#x9a13;">
<node CREATED="1516448792793" ID="ID_590034820" MODIFIED="1516448919993" TEXT="Tree&#x306e;&#x4f5c;&#x6210;&#x65b9;&#x91dd;"/>
<node CREATED="1516448843266" ID="ID_1177321611" MODIFIED="1516454291651" TEXT="&#x8a3c;&#x660e;&#x65b9;&#x91dd;&#x306e;&#x691c;&#x8a0e;,&#x5b9f;&#x88c5;&#x6642;&#x306e;&#x6539;&#x5584;"/>
</node>
<node CREATED="1516448766134" FOLDED="true" ID="ID_712304841" MODIFIED="1517385482976" POSITION="left" TEXT="&#x5b9f;&#x88c5;">
<node CREATED="1516448769994" ID="ID_1122278060" MODIFIED="1516453267632" TEXT="CbC&#x3067;&#x306e;&#x5b9f;&#x88c5;"/>
<node CREATED="1516453268445" ID="ID_1239636691" MODIFIED="1516453272713" TEXT="Agda&#x3067;&#x306e;&#x5b9f;&#x88c5;"/>
<node CREATED="1516453273168" ID="ID_1420286449" MODIFIED="1516454130460" TEXT="Agda&#x3067;&#x306e;&#x8a3c;&#x660e;,&#x89e3;&#x8aac;"/>
</node>
<node CREATED="1516455668900" FOLDED="true" ID="ID_155403381" MODIFIED="1517385484966" POSITION="left" TEXT="&#x8a55;&#x4fa1;">
<node CREATED="1516455671828" ID="ID_1828774278" MODIFIED="1516455677370" TEXT="?"/>
</node>
<node CREATED="1516448787093" FOLDED="true" ID="ID_1477806830" MODIFIED="1517385486194" POSITION="left" TEXT="&#x7d50;&#x8ad6;">
<node CREATED="1516453116787" ID="ID_1750859738" MODIFIED="1516453146188" TEXT="Tree&#x3092;CodeSegment,DataSegment&#x3092;&#x7528;&#x3044;&#x3066;&#x4e8c;&#x3064;&#x306e;&#x8a00;&#x8a9e;&#x3067;&#x8a18;&#x8ff0;&#x3057;&#x305f;"/>
<node CREATED="1516453146841" ID="ID_495843685" MODIFIED="1516695852072" TEXT="&#x7b49;&#x4fa1;&#x306a;&#x30b3;&#x30fc;&#x30c9;&#x304c;&#x3067;&#x304d;&#x305f;?"/>
<node CREATED="1516453179338" ID="ID_710713278" MODIFIED="1516695815136" TEXT="&#x8a3c;&#x660e;&#x652f;&#x63f4;&#x5668;&#x3092;&#x4f7f;&#x3063;&#x3066;unBalance&#x306a;Tree&#x304c;&#x3067;&#x304d;&#x308b;&#x3053;&#x3068;&#x3092;&#x8a3c;&#x660e;&#x3057;&#x305f;?"/>
<node CREATED="1516693502350" ID="ID_1803347987" MODIFIED="1516695887153" TEXT="&#x305d;&#x306e;&#x4ed6;&#x3001;&#x4eca;&#x5f8c;&#x306e;&#x8a71;">
<node CREATED="1516693505485" ID="ID_727445874" MODIFIED="1516693962403" TEXT="CbC&#x306e;&#x30b3;&#x30f3;&#x30d1;&#x30a4;&#x30eb;&#x6642;&#x306b;TypeChecking&#x3082;&#x3067;&#x304d;&#x308b;&#x304b;&#x3082;&#x3057;&#x308c;&#x306a;&#x3044;&#x306d;&#x307f;&#x305f;&#x3044;&#x306a;&#x306f;&#x306a;&#x3057;"/>
</node>
</node>
<node CREATED="1516695662563" ID="ID_1054440656" MODIFIED="1517919043521" POSITION="right" TEXT="&#x7ae0;&#x69cb;&#x6210;">
<node CREATED="1516695644106" ID="ID_736329900" MODIFIED="1517915625719" TEXT="&#x7814;&#x7a76;&#x80cc;&#x666f;">
<node CREATED="1517385504371" ID="ID_201034437" MODIFIED="1517385507130" TEXT="&#x306f;&#x3058;&#x3081;&#x306b;"/>
</node>
<node CREATED="1517384887536" ID="ID_1535504778" MODIFIED="1517915623832" TEXT="CbC">
<node CREATED="1516695675644" ID="ID_922716453" MODIFIED="1517385660735" TEXT="CodeSegment&#x3068;DataSegment"/>
<node CREATED="1517385681042" ID="ID_1583563260" MODIFIED="1517385703041" TEXT="CbC&#x306e;&#x8a18;&#x8ff0;">
<node CREATED="1517385703503" ID="ID_298253554" MODIFIED="1517385713098" TEXT="CbC&#x4e0a;&#x3067;&#x306e;CodeSegment&#x306e;&#x4f8b;"/>
<node CREATED="1517385714282" ID="ID_87445580" MODIFIED="1517385732747" TEXT="CbC&#x4e0a;&#x3067;&#x306e;DataSegment&#x306e;&#x4f8b;"/>
</node>
</node>
<node CREATED="1516695699548" ID="ID_1160729877" MODIFIED="1517919090150" TEXT="&#x8a3c;&#x660e;&#x652f;&#x63f4;&#x7cfb;&#x8a00;&#x8a9e; Agda">
<node CREATED="1517385743439" ID="ID_948325222" MODIFIED="1517385763996" TEXT="Agda&#x6587;&#x6cd5;"/>
<node CREATED="1517385849109" ID="ID_808144723" MODIFIED="1517915747258" TEXT="&#x81ea;&#x7136;&#x6f14;&#x7e79;"/>
<node CREATED="1517385855121" ID="ID_910986235" MODIFIED="1517915747257" TEXT="Curry-Howard&#x540c;&#x578b;&#x5bfe;&#x5fdc;"/>
<node CREATED="1517385877162" ID="ID_869768510" MODIFIED="1517919096406" TEXT="Agda&#x3068;&#x81ea;&#x7136;&#x6f14;&#x7e79;&#x306e;&#x8a3c;&#x660e;&#x306e;&#x4f8b;(&#x305f;&#x3076;&#x3093;&#x4e09;&#x6bb5;&#x8ad6;&#x6cd5;&#x306b;&#x306a;&#x308b;?)"/>
</node>
<node CREATED="1516695693068" ID="ID_1567452235" MODIFIED="1517919073917" TEXT="Agda&#x3067;&#x306e;CodeSegment,DataSegment&#x306e;&#x8868;&#x73fe;">
<node CREATED="1516695675644" ID="ID_1174205441" MODIFIED="1517915886269" TEXT="Agda &#x3067;&#x306e; CodeSegment&#x3001;DataSegment&#x306e;&#x4f8b;"/>
<node CREATED="1516695711821" ID="ID_886806884" MODIFIED="1517385815751" TEXT="Agda &#x3067;&#x306e;Interface&#x90e8;&#x5206;&#x306e;&#x4f8b;"/>
<node CREATED="1517919130739" ID="ID_1483612417" MODIFIED="1517919141847" TEXT="Interface&#x90e8;&#x5206;&#x306e;&#x30de;&#x30c3;&#x30d4;&#x30f3;&#x30b0;"/>
<node CREATED="1517919153166" ID="ID_485244670" MODIFIED="1517919192103" TEXT="SingleLinkedStack &#x306e; Interface"/>
</node>
<node CREATED="1517916349992" ID="ID_239435909" MODIFIED="1517916363169" TEXT="Agda&#x3067;&#x306e;CbC&#x306e;&#x8a3c;&#x660e;">
<node CREATED="1517916008250" ID="ID_1263627528" MODIFIED="1517916370241" TEXT="Hoar-Logic&#x306e;&#x304a;&#x8a71;"/>
<node CREATED="1517919164618" ID="ID_408842432" MODIFIED="1517919173961" TEXT="RedBlackTree &#x306e; Interface"/>
<node CREATED="1517385826823" ID="ID_778238289" MODIFIED="1517916370240" TEXT="Interface&#x90e8;&#x5206;&#x306e;&#x8a3c;&#x660e;(stack,tree)"/>
</node>
<node CREATED="1516695962331" ID="ID_1727743322" MODIFIED="1516695964397" TEXT="&#x307e;&#x3068;&#x3081;">
<node CREATED="1517384473095" ID="ID_1131464081" MODIFIED="1517385933785" TEXT="&#x3044;&#x3044;&#x305f;&#x3044;&#x3068;&#x3053;">
<node CREATED="1517384520003" ID="ID_1024027966" MODIFIED="1517384562444" TEXT="Agda&#x3067;&#x8a18;&#x8ff0;&#x3059;&#x308b;&#x3053;&#x3068;&#x3067;Gears&#x306e;&#x6587;&#x6cd5;&#x7684;&#x66d6;&#x6627;&#x306a;&#x90e8;&#x5206;&#x304c;&#x660e;&#x78ba;&#x5316;&#x3055;&#x308c;&#x305f;"/>
<node CREATED="1517384563497" ID="ID_1552767038" MODIFIED="1517384599221" TEXT="&#x5148;&#x884c;&#x7814;&#x7a76;&#x3068;&#x306e;&#x9055;&#x3044;">
<node CREATED="1517384599498" ID="ID_7745421" MODIFIED="1517384649848" TEXT="&#x30ce;&#x30fc;&#x30de;&#x30eb;&#x30ec;&#x30d9;&#x30eb;&#x3067;&#x306e;&#x30a4;&#x30f3;&#x30bf;&#x30fc;&#x30d5;&#x30a7;&#x30fc;&#x30b9;&#x90e8;&#x5206;&#x306e;&#x8a18;&#x8ff0;"/>
<node CREATED="1517384690992" ID="ID_895803544" MODIFIED="1517384717943" TEXT="&#x30a4;&#x30f3;&#x30bf;&#x30fc;&#x30d5;&#x30a7;&#x30fc;&#x30b9;&#x3092;&#x4f7f;&#x3063;&#x3066;&#x62bd;&#x8c61;&#x5316;&#x3057;&#x305f;(stack,tree))"/>
<node CREATED="1517384651337" ID="ID_1071842343" MODIFIED="1517384658640" TEXT="&#x30a4;&#x30f3;&#x30bf;&#x30fc;&#x30d5;&#x30a7;&#x30fc;&#x30b9;&#x90e8;&#x5206;&#x306e;&#x8a3c;&#x660e;"/>
</node>
</node>
</node>
</node>
</node>
</map>