Mercurial > hg > Papers > 2018 > nozomi-master

view mindmap.mm @ 156:bc9be2d40d0d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add requiremants
author Nozomi Teruya <e125769@ie.u-ryukyu.ac.jp>
date Tue, 30 Jan 2018 23:41:54 +0900
parents 56fe9667efa8
children
line wrap: on
line source

<map version="1.0.1">
<!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net -->
<node CREATED="1482221910478" ID="ID_1754217905" MODIFIED="1482221935755" TEXT="&#x4fee;&#x8ad6;">
<node CREATED="1482221935759" ID="ID_43471633" MODIFIED="1482221939673" POSITION="right" TEXT="&#x30bf;&#x30a4;&#x30c8;&#x30eb;">
<node CREATED="1482221939675" ID="ID_1296789347" MODIFIED="1482221950529" TEXT="Type System of Continuation based C"/>
<node CREATED="1482222651209" ID="ID_461835641" MODIFIED="1482222661597" TEXT="verification methods of Continuation based"/>
</node>
<node CREATED="1482221990937" FOLDED="true" ID="ID_1386275252" MODIFIED="1482223391657" POSITION="left" TEXT="CbC">
<node CREATED="1482221993693" ID="ID_715381022" MODIFIED="1482221997710" TEXT="GearsOS">
<node CREATED="1482222011168" ID="ID_730492008" MODIFIED="1482222013581" TEXT="CodeGear"/>
<node CREATED="1482222013828" ID="ID_376534265" MODIFIED="1482222015436" TEXT="DataGear"/>
</node>
<node CREATED="1482222007269" ID="ID_799040958" MODIFIED="1482222282037" TEXT="target">
<node CREATED="1482222282038" ID="ID_1200540305" MODIFIED="1482222291997" TEXT="embedded systems">
<node CREATED="1482222291998" ID="ID_1155059144" MODIFIED="1482222301101" TEXT="as architecture independent assembler"/>
</node>
</node>
<node CREATED="1482222016940" ID="ID_580020090" MODIFIED="1482222019983" TEXT="Meta Computations">
<node CREATED="1482222020617" ID="ID_889133880" MODIFIED="1482222021834" TEXT="goto"/>
<node CREATED="1482222022059" ID="ID_399619212" MODIFIED="1482222030432" TEXT="memory allocation"/>
<node CREATED="1482222030824" ID="ID_1991044142" MODIFIED="1482222035273" TEXT="verification">
<node CREATED="1482222036316" ID="ID_580529409" MODIFIED="1482222037661" TEXT="model check">
<node CREATED="1482222453168" ID="ID_1183894986" MODIFIED="1482222456387" TEXT="using itself"/>
<node CREATED="1482222458636" ID="ID_847927718" MODIFIED="1482222467074" TEXT="convert to verifiable language">
<node CREATED="1482222467075" ID="ID_498881041" MODIFIED="1482222469271" TEXT="cbmc"/>
</node>
</node>
<node CREATED="1482222037895" ID="ID_1425357343" MODIFIED="1482222038741" TEXT="proof">
<node CREATED="1482222438684" ID="ID_1227239485" MODIFIED="1482222442387" TEXT="using itself"/>
<node CREATED="1482222442683" ID="ID_1450250056" MODIFIED="1482222447146" TEXT="another language"/>
</node>
</node>
<node CREATED="1482222225427" ID="ID_1863901686" MODIFIED="1482222227129" TEXT="stub"/>
<node CREATED="1482222229712" ID="ID_715526680" MODIFIED="1482222231789" TEXT="open system"/>
</node>
<node CREATED="1482221997960" ID="ID_1972351768" MODIFIED="1482222003575" TEXT="CodeSegment">
<node CREATED="1482222253509" ID="ID_1734116065" MODIFIED="1482222272375" TEXT="tail call  only"/>
<node CREATED="1482222544810" ID="ID_745453988" MODIFIED="1482222555546" TEXT="composability">
<node CREATED="1482222555547" ID="ID_1704453545" MODIFIED="1482222564855" TEXT="run-time connection">
<node CREATED="1482222588858" ID="ID_1106262807" MODIFIED="1482222593248" TEXT="like Alice?"/>
</node>
<node CREATED="1482222566356" ID="ID_352025867" MODIFIED="1482222570805" TEXT="compile-time connection">
<node CREATED="1482222570806" ID="ID_1629059714" MODIFIED="1482222574256" TEXT="make"/>
<node CREATED="1482222574505" ID="ID_553014003" MODIFIED="1482222583672" TEXT="linker"/>
</node>
</node>
</node>
<node CREATED="1482222003793" ID="ID_934649172" MODIFIED="1482222005578" TEXT="DataSegment">
<node CREATED="1482222234205" ID="ID_1162486321" MODIFIED="1482222250539" TEXT="union of struct"/>
</node>
<node CREATED="1482222310973" ID="ID_480941648" MODIFIED="1482222484423" TEXT="purpose">
<node CREATED="1482222485077" ID="ID_1256707103" MODIFIED="1482222493654" TEXT="parallel"/>
<node CREATED="1482222494038" ID="ID_1057807575" MODIFIED="1482222529460" TEXT="reliance"/>
<node CREATED="1482222523357" ID="ID_1553645063" MODIFIED="1482222523357" TEXT=""/>
</node>
<node CREATED="1482222598543" ID="ID_333333590" MODIFIED="1482222600955" TEXT="executables">
<node CREATED="1482222600956" ID="ID_937738784" MODIFIED="1482222606772" TEXT="red-black tree"/>
<node CREATED="1482222607058" ID="ID_441757614" MODIFIED="1482222646166" TEXT="synchronized queue"/>
</node>
</node>
<node CREATED="1482222701114" FOLDED="true" ID="ID_1128453777" MODIFIED="1482223428054" POSITION="right" TEXT="Type System">
<node CREATED="1482222703166" ID="ID_1131357019" MODIFIED="1482222709834" TEXT="simple type">
<node CREATED="1482222709835" ID="ID_1320515160" MODIFIED="1482222716172" TEXT="lambda calculs">
<node CREATED="1482222716173" ID="ID_764423043" MODIFIED="1482222723728" TEXT="alpha conversion"/>
<node CREATED="1482222724026" ID="ID_836760115" MODIFIED="1482222726684" TEXT="beta reduction"/>
<node CREATED="1482222728845" ID="ID_1689964966" MODIFIED="1482222731501" TEXT="de brujin index"/>
<node CREATED="1482222733647" ID="ID_1888263821" MODIFIED="1482222739271" TEXT="literals"/>
<node CREATED="1482222739526" ID="ID_102897226" MODIFIED="1482222741467" TEXT="definitions">
<node CREATED="1482222742985" ID="ID_355936501" MODIFIED="1482222744367" TEXT="variable"/>
<node CREATED="1482222744612" ID="ID_410323730" MODIFIED="1482222747132" TEXT="abstraction"/>
<node CREATED="1482222747420" ID="ID_1932069881" MODIFIED="1482222748843" TEXT="application"/>
</node>
</node>
<node CREATED="1482222750392" ID="ID_240081393" MODIFIED="1482222761056" TEXT="types">
<node CREATED="1482222761057" ID="ID_1784300464" MODIFIED="1482222762584" TEXT="base type">
<node CREATED="1482222762585" ID="ID_180979318" MODIFIED="1482222763121" TEXT="int"/>
<node CREATED="1482222763420" ID="ID_958834276" MODIFIED="1482222764756" TEXT="char"/>
</node>
<node CREATED="1482222768335" ID="ID_1789225146" MODIFIED="1482222876437" TEXT="&#x7528;&#x8a9e;&#x5fd8;&#x308c;&#x305f;">
<node CREATED="1482222876438" ID="ID_718205970" MODIFIED="1482222877702" TEXT="sum"/>
<node CREATED="1482222877894" ID="ID_911219949" MODIFIED="1482222878959" TEXT="product"/>
<node CREATED="1482222879171" ID="ID_310699645" MODIFIED="1482222881609" TEXT="list"/>
</node>
</node>
</node>
<node CREATED="1482222884176" ID="ID_45203894" MODIFIED="1482222896720" TEXT="subtype"/>
<node CREATED="1482222962289" ID="ID_1055304856" MODIFIED="1482222979908" TEXT="generic type"/>
<node CREATED="1482222834747" ID="ID_696024551" MODIFIED="1482222840842" TEXT="type inference algorithms">
<node CREATED="1482222840843" ID="ID_197920761" MODIFIED="1482222845213" TEXT="algorithm W"/>
<node CREATED="1482222845427" ID="ID_1889623223" MODIFIED="1482222849546" TEXT="Hindly-Milner"/>
</node>
</node>
<node CREATED="1482223001279" ID="ID_352118659" MODIFIED="1482223007803" POSITION="left" TEXT="model checking">
<node CREATED="1482223008161" ID="ID_360203122" MODIFIED="1482223014473" TEXT="symbolic">
<node CREATED="1482223014474" ID="ID_1160976375" MODIFIED="1482223016995" TEXT="cbmc"/>
</node>
<node CREATED="1482223078731" ID="ID_283009196" MODIFIED="1482223079850" TEXT="akasha">
<node CREATED="1482223084863" ID="ID_1872994741" MODIFIED="1482223100550" TEXT="Brute-force"/>
</node>
</node>
<node CREATED="1482223018734" ID="ID_41404581" MODIFIED="1482223021822" POSITION="right" TEXT="proofs">
<node CREATED="1482223021823" ID="ID_233838165" MODIFIED="1482223027612" TEXT="systemF"/>
<node CREATED="1482223027964" ID="ID_1544350887" MODIFIED="1482223052084" TEXT="Curry-Howard Isomorphism"/>
<node CREATED="1482223056992" ID="ID_1107619493" MODIFIED="1482223063552" TEXT="natural deduction"/>
<node CREATED="1482223116497" ID="ID_1653251645" MODIFIED="1482223119546" TEXT="first-order logic"/>
<node CREATED="1482223408151" ID="ID_852684181" MODIFIED="1482223409546" TEXT="category">
<node CREATED="1482223417849" ID="ID_127770600" MODIFIED="1482223422926" TEXT="object"/>
<node CREATED="1482223423183" ID="ID_1930419478" MODIFIED="1482223424937" TEXT="morphism"/>
<node CREATED="1482223409547" ID="ID_943630535" MODIFIED="1482223412609" TEXT="functor"/>
<node CREATED="1482223412853" ID="ID_1513870177" MODIFIED="1482223416614" TEXT="monad"/>
</node>
</node>
<node CREATED="1482223143899" ID="ID_1616397445" MODIFIED="1482223184489" POSITION="left" TEXT="on going">
<node CREATED="1482223185040" ID="ID_52304753" MODIFIED="1482223199912" TEXT="define type system of cbc">
<node CREATED="1482223199913" ID="ID_1586295609" MODIFIED="1482223200934" TEXT="agda"/>
<node CREATED="1482223201171" ID="ID_91193408" MODIFIED="1482223204915" TEXT="simple type"/>
<node CREATED="1482223205147" ID="ID_1398078904" MODIFIED="1482223208478" TEXT="sub type"/>
<node CREATED="1482223298624" ID="ID_976150345" MODIFIED="1482223305634" TEXT="code segment composition"/>
</node>
<node CREATED="1482223211660" ID="ID_1152569760" MODIFIED="1482223226516" TEXT="generate stub/ds">
<node CREATED="1482223226517" ID="ID_1105412168" MODIFIED="1482223231562" TEXT="from type informations"/>
</node>
<node CREATED="1482223232935" ID="ID_1561456436" MODIFIED="1482223246635" TEXT="proof red-black tree"/>
<node CREATED="1482223256853" ID="ID_1762699523" MODIFIED="1482223312589" TEXT="type system as meta computations">
<node CREATED="1482223312590" ID="ID_1169523272" MODIFIED="1482223336401" TEXT="swap composition implementation"/>
<node CREATED="1482223336909" ID="ID_239798407" MODIFIED="1482223368583" TEXT="prove commutativity of composition">
<node CREATED="1482223445928" ID="ID_308200047" MODIFIED="1482223447673" TEXT="like monad"/>
</node>
</node>
</node>
</node>
</map>