<map version="freeplane 1.9.13">
<!--To view this file, download free mind mapping software Freeplane from https://www.freeplane.org -->
<node TEXT="rbtree-gearsagda" FOLDED="false" ID="ID_452131666" CREATED="1610381621610" MODIFIED="1681354145545" STYLE="oval">
<font SIZE="18"/>
<hook NAME="MapStyle" zoom="0.75">
    <properties edgeColorConfiguration="#808080ff,#ff0000ff,#0000ffff,#00ff00ff,#ff00ffff,#00ffffff,#7c0000ff,#00007cff,#007c00ff,#7c007cff,#007c7cff,#7c7c00ff" fit_to_viewport="false" associatedTemplateLocation="template:/standard-1.6-noEdgeColor.mm" show_icon_for_attributes="true" show_note_icons="true"/>

<map_styles>
<stylenode LOCALIZED_TEXT="styles.root_node" STYLE="oval" UNIFORM_SHAPE="true" VGAP_QUANTITY="24 pt">
<font SIZE="24"/>
<stylenode LOCALIZED_TEXT="styles.predefined" POSITION="right" STYLE="bubble">
<stylenode LOCALIZED_TEXT="default" ID="ID_207122690" COLOR="#000000" STYLE="fork">
<arrowlink SHAPE="CUBIC_CURVE" COLOR="#000000" WIDTH="2" TRANSPARENCY="200" DASH="" FONT_SIZE="9" FONT_FAMILY="SansSerif" DESTINATION="ID_207122690" STARTARROW="NONE" ENDARROW="DEFAULT"/>
<font NAME="SansSerif" SIZE="10" BOLD="false" ITALIC="false"/>
<richcontent CONTENT-TYPE="plain/auto" TYPE="DETAILS"/>
<richcontent TYPE="NOTE" CONTENT-TYPE="plain/auto"/>
</stylenode>
<stylenode LOCALIZED_TEXT="defaultstyle.details"/>
<stylenode LOCALIZED_TEXT="defaultstyle.attributes">
<font SIZE="9"/>
</stylenode>
<stylenode LOCALIZED_TEXT="defaultstyle.note" COLOR="#000000" BACKGROUND_COLOR="#ffffff" TEXT_ALIGN="LEFT"/>
<stylenode LOCALIZED_TEXT="defaultstyle.floating">
<edge STYLE="hide_edge"/>
<cloud COLOR="#f0f0f0" SHAPE="ROUND_RECT"/>
</stylenode>
<stylenode LOCALIZED_TEXT="defaultstyle.selection" BACKGROUND_COLOR="#afd3f7" BORDER_COLOR_LIKE_EDGE="false" BORDER_COLOR="#afd3f7"/>
</stylenode>
<stylenode LOCALIZED_TEXT="styles.user-defined" POSITION="right" STYLE="bubble">
<stylenode LOCALIZED_TEXT="styles.topic" COLOR="#18898b" STYLE="fork">
<font NAME="Liberation Sans" SIZE="10" BOLD="true"/>
</stylenode>
<stylenode LOCALIZED_TEXT="styles.subtopic" COLOR="#cc3300" STYLE="fork">
<font NAME="Liberation Sans" SIZE="10" BOLD="true"/>
</stylenode>
<stylenode LOCALIZED_TEXT="styles.subsubtopic" COLOR="#669900">
<font NAME="Liberation Sans" SIZE="10" BOLD="true"/>
</stylenode>
<stylenode LOCALIZED_TEXT="styles.important" ID="ID_3752836">
<icon BUILTIN="yes"/>
<arrowlink COLOR="#003399" TRANSPARENCY="255" DESTINATION="ID_3752836"/>
</stylenode>
</stylenode>
<stylenode LOCALIZED_TEXT="styles.AutomaticLayout" POSITION="right" STYLE="bubble">
<stylenode LOCALIZED_TEXT="AutomaticLayout.level.root" COLOR="#000000" STYLE="oval" SHAPE_HORIZONTAL_MARGIN="10 pt" SHAPE_VERTICAL_MARGIN="10 pt">
<font SIZE="18"/>
</stylenode>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,1" COLOR="#0033ff">
<font SIZE="16"/>
</stylenode>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,2" COLOR="#00b439">
<font SIZE="14"/>
</stylenode>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,3" COLOR="#990000">
<font SIZE="12"/>
</stylenode>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,4" COLOR="#111111">
<font SIZE="10"/>
</stylenode>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,5"/>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,6"/>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,7"/>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,8"/>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,9"/>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,10"/>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,11"/>
</stylenode>
</stylenode>
</map_styles>
</hook>
<node TEXT="GearAgdanによるRed Black Tree の検証" POSITION="right" ID="ID_1707429913" CREATED="1681354146375" MODIFIED="1681354149504"/>
<node TEXT="Gears OS" POSITION="left" ID="ID_1627768067" CREATED="1681370097231" MODIFIED="1681370135147">
<node TEXT="Continuation based C" ID="ID_886365419" CREATED="1681370135452" MODIFIED="1681370144727"/>
<node TEXT="CodeGear and DataGear" ID="ID_1505619678" CREATED="1681370145576" MODIFIED="1681370169360"/>
<node TEXT="GearsAgda" ID="ID_1483093782" CREATED="1681370170247" MODIFIED="1681370174624"/>
<node TEXT="lightweigt continuation" ID="ID_709373441" CREATED="1681370232271" MODIFIED="1681370241482"/>
</node>
<node TEXT="meta computation" POSITION="left" ID="ID_587222105" CREATED="1681370246638" MODIFIED="1681370255183">
<node TEXT="IO" ID="ID_939386664" CREATED="1681370255664" MODIFIED="1681370261532"/>
<node TEXT="Hoare Logic" ID="ID_468705414" CREATED="1681370262977" MODIFIED="1681370270967"/>
</node>
<node TEXT="meata computation in GearsAgda" POSITION="left" ID="ID_1679966111" CREATED="1681370285647" MODIFIED="1681370300383">
<node TEXT="Gears Form" ID="ID_562028595" CREATED="1681370303175" MODIFIED="1681370328863"/>
<node TEXT="Meta computation" ID="ID_532649685" CREATED="1681370334319" MODIFIED="1681370340118"/>
<node TEXT="Segment" ID="ID_1391622726" CREATED="1681370342818" MODIFIED="1681370346242"/>
<node TEXT="stub" ID="ID_1481524131" CREATED="1681370347413" MODIFIED="1681370350369"/>
<node TEXT="CodeGear table" ID="ID_528079968" CREATED="1681370352629" MODIFIED="1681370366378"/>
</node>
<node TEXT="Hoare Logic" POSITION="left" ID="ID_590542814" CREATED="1681370375413" MODIFIED="1681370379970">
<node TEXT="command base" ID="ID_1041738747" CREATED="1681370380249" MODIFIED="1681370383059"/>
<node TEXT="first order" ID="ID_1511997811" CREATED="1681370399684" MODIFIED="1681370403829"/>
<node TEXT="soundness" ID="ID_783227970" CREATED="1681370407410" MODIFIED="1681370413286">
<node TEXT="separated from program" ID="ID_549960702" CREATED="1681370413548" MODIFIED="1681370423487"/>
</node>
<node TEXT="no proof support" ID="ID_94897053" CREATED="1681370433921" MODIFIED="1681370438778"/>
</node>
<node TEXT="GearsAgda" POSITION="left" ID="ID_613685836" CREATED="1681370441463" MODIFIED="1681370446502">
<node TEXT="written in Agda" ID="ID_883451142" CREATED="1681370450642" MODIFIED="1681370456415">
<node TEXT="proof assistance" ID="ID_567095247" CREATED="1681370456760" MODIFIED="1681370462431"/>
</node>
<node TEXT="any lightweight continuation form" ID="ID_512231980" CREATED="1681370472049" MODIFIED="1681370490394"/>
<node TEXT="close to basic unit in a compiler" ID="ID_1639405885" CREATED="1681370493600" MODIFIED="1681370507300"/>
<node TEXT="concurrency" ID="ID_1969768669" CREATED="1681370510538" MODIFIED="1681370522360"/>
<node TEXT="meta computation" ID="ID_1341787488" CREATED="1681370523208" MODIFIED="1681370528202">
<node TEXT="Hoare Logic style" ID="ID_1596917933" CREATED="1681370535368" MODIFIED="1681370546348"/>
<node TEXT="with invariant" ID="ID_1946393368" CREATED="1681370547204" MODIFIED="1681370553272"/>
</node>
<node TEXT="data with proofs" ID="ID_1144050858" CREATED="1681370596859" MODIFIED="1681370601940">
<node TEXT="invariant" ID="ID_375933480" CREATED="1681370605320" MODIFIED="1681370610877"/>
<node TEXT="much simpler" ID="ID_245103686" CREATED="1681370613781" MODIFIED="1681370622639"/>
</node>
</node>
<node TEXT="concurrency" POSITION="right" ID="ID_1659998734" CREATED="1681370628915" MODIFIED="1681370636745">
<node TEXT="codeGear-wise concurency" ID="ID_1216124303" CREATED="1681370637291" MODIFIED="1681370656059"/>
<node TEXT="assuming  finite computation in a codeGear" ID="ID_573537896" CREATED="1681370657029" MODIFIED="1681370677168"/>
<node TEXT="scheduler" ID="ID_327350914" CREATED="1681370679365" MODIFIED="1681370685685">
<node TEXT="in meta computation" ID="ID_1272612921" CREATED="1681370686271" MODIFIED="1681370693104"/>
<node TEXT="code table" ID="ID_1779321838" CREATED="1681370741527" MODIFIED="1681370746964">
<node TEXT="all codeGear" ID="ID_1073597539" CREATED="1681370747218" MODIFIED="1681370752548"/>
<node TEXT="numbered" ID="ID_1618653220" CREATED="1681370753308" MODIFIED="1681370756196"/>
<node TEXT="stub" ID="ID_573578192" CREATED="1681370756935" MODIFIED="1681370759362"/>
</node>
<node TEXT="Context" ID="ID_1995851564" CREATED="1681370693516" MODIFIED="1681370697602">
<node TEXT="current code" ID="ID_1885258842" CREATED="1681370728219" MODIFIED="1681370732220"/>
<node TEXT="all dataGear" ID="ID_1859577487" CREATED="1681370733587" MODIFIED="1681370739913"/>
</node>
<node TEXT="communication" ID="ID_387799092" CREATED="1681370705533" MODIFIED="1681370712647"/>
</node>
<node TEXT="model checking" ID="ID_1191776209" CREATED="1681370766180" MODIFIED="1681370771240"/>
<node TEXT="proofs on concurrenct" ID="ID_1117350246" CREATED="1681370771658" MODIFIED="1681370781273"/>
</node>
<node TEXT="while program" POSITION="right" ID="ID_710382637" CREATED="1681370805471" MODIFIED="1681370811890"/>
<node TEXT="binary tree" POSITION="right" ID="ID_1922786513" CREATED="1681370796432" MODIFIED="1681370804204">
<node TEXT="stack invariant" ID="ID_1448419661" CREATED="1681370821482" MODIFIED="1681370830261"/>
<node TEXT="tree invariant" ID="ID_243832132" CREATED="1681370830768" MODIFIED="1681370835246"/>
<node TEXT="replace invariant" ID="ID_1303870466" CREATED="1681370835840" MODIFIED="1681370840736"/>
</node>
<node TEXT="red black tree" POSITION="right" ID="ID_263237724" CREATED="1681370787198" MODIFIED="1681370792658">
<node TEXT="red and black" ID="ID_385223552" CREATED="1681370848145" MODIFIED="1681370856270"/>
<node TEXT="parent and grand parent" ID="ID_517970079" CREATED="1681370857076" MODIFIED="1681370866920">
<node TEXT="in stack" ID="ID_901165358" CREATED="1681370867215" MODIFIED="1681370872234"/>
</node>
<node TEXT="concurrency" ID="ID_23246060" CREATED="1681370878663" MODIFIED="1681370883733">
<node TEXT="root replacement" ID="ID_184711355" CREATED="1681370884231" MODIFIED="1681370892725">
<node TEXT="transaction" ID="ID_1256246418" CREATED="1681370893169" MODIFIED="1681370898372"/>
</node>
<node TEXT="non destructive" ID="ID_1377710910" CREATED="1681370903423" MODIFIED="1681370909214">
<node TEXT="read sharing" ID="ID_1853077777" CREATED="1681370910265" MODIFIED="1681370917627"/>
</node>
</node>
</node>
<node TEXT="complied code" POSITION="right" ID="ID_1551916219" CREATED="1681370926034" MODIFIED="1681370931197">
<node TEXT="gearsAgda  →　CbC conversion" ID="ID_159756131" CREATED="1681370931496" MODIFIED="1681370953438"/>
<node TEXT="combine multiple codeGear" ID="ID_1952851358" CREATED="1681371036240" MODIFIED="1681371047551">
<node TEXT="optimization" ID="ID_256515995" CREATED="1681371048689" MODIFIED="1681371053081"/>
</node>
</node>
<node TEXT="is this reliable?" POSITION="right" ID="ID_189224322" CREATED="1681370969828" MODIFIED="1681370979059">
<node TEXT="with proofs" ID="ID_114174861" CREATED="1681370979357" MODIFIED="1681370985340">
<node TEXT="relative to the theory" ID="ID_194349290" CREATED="1681370985587" MODIFIED="1681371003316"/>
</node>
<node TEXT="invariant gives all property" ID="ID_955091732" CREATED="1681371007176" MODIFIED="1681371020551"/>
</node>
<node TEXT="is this scale?" POSITION="right" ID="ID_1442547192" CREATED="1681371022394" MODIFIED="1681371028550">
<node TEXT="size of invariant" ID="ID_66636375" CREATED="1681470579922" MODIFIED="1681470584136"/>
<node TEXT="polynominal of cases of invariant" ID="ID_1431513531" CREATED="1681470584691" MODIFIED="1681470597800"/>
<node TEXT="not all combination is possible" ID="ID_1626555105" CREATED="1681470604805" MODIFIED="1681470612527"/>
<node TEXT="we don&apos;t need to fill all the proof" ID="ID_1601614737" CREATED="1681470615256" MODIFIED="1681470627377">
<node TEXT="incremental" ID="ID_1230800920" CREATED="1681470627899" MODIFIED="1681470630690"/>
<node TEXT="partial" ID="ID_649982266" CREATED="1681470631099" MODIFIED="1681470634557"/>
</node>
</node>
<node TEXT="contents" POSITION="right" ID="ID_1884614552" CREATED="1681470012072" MODIFIED="1681470018912">
<node TEXT="verified red black tree" ID="ID_72137676" CREATED="1681470019151" MODIFIED="1681470047634"/>
<node TEXT="importance" ID="ID_510340227" CREATED="1681470049510" MODIFIED="1681470056562">
<node TEXT="conversion to classical form" ID="ID_312471113" CREATED="1681470523375" MODIFIED="1681470532568">
<node TEXT="destructive" ID="ID_1083852390" CREATED="1681470532868" MODIFIED="1681470536236"/>
<node TEXT="B-tree" ID="ID_1942790971" CREATED="1681470545925" MODIFIED="1681470551384"/>
</node>
<node TEXT="sequencial" ID="ID_783108258" CREATED="1681470056922" MODIFIED="1681470064048"/>
<node TEXT="concurrent" ID="ID_924506929" CREATED="1681470065130" MODIFIED="1681470068278"/>
</node>
<node TEXT="GearsAgda" ID="ID_1614171466" CREATED="1681470071381" MODIFIED="1681470074368">
<node TEXT="lightweight contination" ID="ID_351064745" CREATED="1681470074675" MODIFIED="1681470097157"/>
<node TEXT="CbC" ID="ID_280197854" CREATED="1681470108615" MODIFIED="1681470110151"/>
</node>
<node TEXT="classical approach" ID="ID_439782904" CREATED="1681470111745" MODIFIED="1681470120213">
<node TEXT="Hoare Logic" ID="ID_182843234" CREATED="1681470120549" MODIFIED="1681470123261"/>
<node TEXT="conversion to Haskell" ID="ID_18215857" CREATED="1681470123809" MODIFIED="1681470131336"/>
<node TEXT="verified but ..." ID="ID_86587986" CREATED="1681470188224" MODIFIED="1681470199159"/>
</node>
<node TEXT="GearsAgda" ID="ID_1624783880" CREATED="1681470180677" MODIFIED="1681470219506">
<node TEXT="invariant" ID="ID_1822140966" CREATED="1681470228788" MODIFIED="1681470232318">
<node TEXT="denotational semantics" ID="ID_1070066378" CREATED="1681470408330" MODIFIED="1681470415583"/>
</node>
<node TEXT="agda introduction" ID="ID_1367482138" CREATED="1681470219860" MODIFIED="1681470227830"/>
<node TEXT="simple while loop" ID="ID_594789165" CREATED="1681470293741" MODIFIED="1681470299458"/>
<node TEXT="loop connector" ID="ID_351381557" CREATED="1681470305517" MODIFIED="1681470311087">
<node TEXT="reduction parameter" ID="ID_1854148894" CREATED="1681470317762" MODIFIED="1681470324065"/>
</node>
</node>
<node TEXT="binary tree" ID="ID_1045767712" CREATED="1681470238269" MODIFIED="1681470245777">
<node TEXT="invariant" ID="ID_753395200" CREATED="1681470246095" MODIFIED="1681470248201">
<node TEXT="tree" ID="ID_1179203442" CREATED="1681470248688" MODIFIED="1681470254441"/>
<node TEXT="stack" ID="ID_743804922" CREATED="1681470255070" MODIFIED="1681470256626"/>
<node TEXT="replace" ID="ID_1919439558" CREATED="1681470257216" MODIFIED="1681470260232"/>
</node>
<node TEXT="program guidance" ID="ID_1331715304" CREATED="1681470429863" MODIFIED="1681470434889">
<node TEXT="differential of invariant" ID="ID_1547779379" CREATED="1681470435636" MODIFIED="1681470444235"/>
</node>
</node>
<node TEXT="red black tree" ID="ID_233668516" CREATED="1681470263078" MODIFIED="1681470266745"/>
<node TEXT="concurrency" ID="ID_1836297821" CREATED="1681470271427" MODIFIED="1681470275872">
<node TEXT="segmented" ID="ID_290000164" CREATED="1681470276209" MODIFIED="1681470282080"/>
<node TEXT="code table" ID="ID_278977606" CREATED="1681470350363" MODIFIED="1681470354017"/>
<node TEXT="scheduler" ID="ID_111624804" CREATED="1681470354785" MODIFIED="1681470364123">
<node TEXT="fairness" ID="ID_1334406786" CREATED="1681470365738" MODIFIED="1681470368781"/>
</node>
<node TEXT="temporal logic" ID="ID_1823540844" CREATED="1681470371933" MODIFIED="1681470376053"/>
</node>
<node TEXT="execution" ID="ID_95297285" CREATED="1681470455878" MODIFIED="1681470458355">
<node TEXT="data gear with proof is executable" ID="ID_1369250602" CREATED="1681470459700" MODIFIED="1681470472621"/>
<node TEXT="need not to fill the proof" ID="ID_1356375326" CREATED="1681470474612" MODIFIED="1681470483972"/>
</node>
<node TEXT="scalability" ID="ID_1468980711" CREATED="1681470382482" MODIFIED="1681470389280">
<node TEXT="invariant library" ID="ID_1421089406" CREATED="1681470391295" MODIFIED="1681470395791"/>
</node>
</node>
</node>
</map>