Mercurial > hg > Papers > 2018 > ryokka-sigos

view thesis.mm @ 8:35d15c091cfd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix Makefile export .agda.replaced,and main document
author ryokka
date Mon, 23 Apr 2018 21:44:32 +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>