{
    "root": {
        "data": {
            "id": "cgxlfherlow0",
            "created": 1641370916386,
            "text": "Geas Agda による Red Black Tree の検証",
            "expandState": "expand",
            "font-family": "arial,helvetica,sans-serif",
            "font-size": 48
        },
        "children": [
            {
                "data": {
                    "id": "cgxlfx0m2z40",
                    "created": 1641370950359,
                    "text": "検証を考慮したプログラミング",
                    "expandState": "collapse",
                    "font-family": "arial,helvetica,sans-serif",
                    "font-size": 48,
                    "layout": null
                },
                "children": [
                    {
                        "data": {
                            "id": "cgxlgipyuxs0",
                            "created": 1641370997605,
                            "text": "normal level",
                            "expandState": "expand",
                            "layout": null,
                            "font-size": 48
                        },
                        "children": [
                            {
                                "data": {
                                    "id": "cgxlhrjs4k00",
                                    "created": 1641371095186,
                                    "text": "軽量継続",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxli256q000",
                                    "created": 1641371118248,
                                    "text": "ポインタなし",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxlim5c3sg0",
                                    "created": 1641371161793,
                                    "text": "atomic",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxllg38ymg0",
                                    "created": 1641371383698,
                                    "text": "関数型",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": [
                                    {
                                        "data": {
                                            "id": "cgxllmgvr800",
                                            "created": 1641371397583,
                                            "text": "input",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    },
                                    {
                                        "data": {
                                            "id": "cgxllqrjogw0",
                                            "created": 1641371406935,
                                            "text": "output",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    }
                                ]
                            }
                        ]
                    },
                    {
                        "data": {
                            "id": "cgxlgq5zx1s0",
                            "created": 1641371013811,
                            "text": "meta level",
                            "expandState": "expand",
                            "layout": null,
                            "font-size": 48
                        },
                        "children": [
                            {
                                "data": {
                                    "id": "cgxliu7bxrk0",
                                    "created": 1641371179328,
                                    "text": "context",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": [
                                    {
                                        "data": {
                                            "id": "cgxllxthvds0",
                                            "created": 1641371422291,
                                            "text": "すべてのData Gear",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    },
                                    {
                                        "data": {
                                            "id": "cgxlm47uykg0",
                                            "created": 1641371436220,
                                            "text": "すべてのCode Gear",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    },
                                    {
                                        "data": {
                                            "id": "cgxlmkb2o800",
                                            "created": 1641371471243,
                                            "text": "process",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    }
                                ]
                            },
                            {
                                "data": {
                                    "id": "cgxlj2hbn9k0",
                                    "created": 1641371197346,
                                    "text": "証明",
                                    "expandState": "expand",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": [
                                    {
                                        "data": {
                                            "id": "cgxljjm4m9s0",
                                            "created": 1641371234642,
                                            "text": "Hoare Condition",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    },
                                    {
                                        "data": {
                                            "id": "cgxljmev1280",
                                            "created": 1641371240733,
                                            "text": "Invariant",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": [
                                            {
                                                "data": {
                                                    "id": "cgxlmsv14oo0",
                                                    "created": 1641371489864,
                                                    "text": "meta Input Data Gear",
                                                    "layout": null,
                                                    "font-size": 48
                                                },
                                                "children": []
                                            }
                                        ]
                                    }
                                ]
                            },
                            {
                                "data": {
                                    "id": "cgxlkgz1ygo0",
                                    "created": 1641371307257,
                                    "text": "memory 管理",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxlkly512o0",
                                    "created": 1641371318086,
                                    "text": "並列実行",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxlkqjjn4g0",
                                    "created": 1641371328087,
                                    "text": "ポインタ",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxll4ohduw0",
                                    "created": 1641371358861,
                                    "text": "monad",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            }
                        ]
                    },
                    {
                        "data": {
                            "id": "cgxlgvirsns0",
                            "created": 1641371025468,
                            "text": "実装記述",
                            "layout": null,
                            "font-size": 48
                        },
                        "children": [
                            {
                                "data": {
                                    "id": "cgxlhfa33qg0",
                                    "created": 1641371068478,
                                    "text": "Gears Agda",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": [
                                    {
                                        "data": {
                                            "id": "cgxlnho65fs0",
                                            "created": 1641371543868,
                                            "text": "Agdaでの決まった形式",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": [
                                            {
                                                "data": {
                                                    "id": "cgxlnq7nxyg0",
                                                    "created": 1641371562461,
                                                    "text": "→ t",
                                                    "layout": null,
                                                    "font-size": 48
                                                },
                                                "children": []
                                            }
                                        ]
                                    },
                                    {
                                        "data": {
                                            "id": "cgxloa4qg0w0",
                                            "created": 1641371605820,
                                            "text": "証明しやすい記述",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    }
                                ]
                            },
                            {
                                "data": {
                                    "id": "cgxlhipmiew0",
                                    "created": 1641371075948,
                                    "text": "CbC",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": [
                                    {
                                        "data": {
                                            "id": "cgxlk75b1fs0",
                                            "created": 1641371285867,
                                            "text": "Cと同じ実行速度",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    },
                                    {
                                        "data": {
                                            "id": "cgxlnvokqhk0",
                                            "created": 1641371574368,
                                            "text": "__code goto",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    },
                                    {
                                        "data": {
                                            "id": "cgxlofzu3co0",
                                            "created": 1641371618584,
                                            "text": "実行効率が良いように記述",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    }
                                ]
                            }
                        ]
                    },
                    {
                        "data": {
                            "id": "cgxlgzsut080",
                            "created": 1641371034785,
                            "text": "実装+証明",
                            "expandState": "expand",
                            "layout": null,
                            "font-size": 48
                        },
                        "children": [
                            {
                                "data": {
                                    "id": "cgxloqvtips0",
                                    "created": 1641371642286,
                                    "text": "Gears Agda 上でnormal level で Hoare Condition をつけた形で記述",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxlphv589s0",
                                    "created": 1641371701018,
                                    "text": "loop を接続する Meta Gear を用意する",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": [
                                    {
                                        "data": {
                                            "id": "cgxlptuvpso0",
                                            "created": 1641371727124,
                                            "text": "停止性の証明も行う",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    }
                                ]
                            },
                            {
                                "data": {
                                    "id": "cgxlq1suwxc0",
                                    "created": 1641371744416,
                                    "text": "Hoare Condition が接続されれば証明は完成",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": [
                                    {
                                        "data": {
                                            "id": "cgxlqsfels00",
                                            "created": 1641371802376,
                                            "text": "Meta Gear を証明を値として与えているから",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    }
                                ]
                            },
                            {
                                "data": {
                                    "id": "cgxlub15o9s0",
                                    "created": 1641372077966,
                                    "text": "並列実行の証明は複数のContextのinter leave",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            }
                        ]
                    },
                    {
                        "data": {
                            "id": "cgxlrlr5ly00",
                            "created": 1641371866213,
                            "text": "仕様記述",
                            "expandState": "expand",
                            "layout": null,
                            "font-size": 48
                        },
                        "children": [
                            {
                                "data": {
                                    "id": "cgxlrwcghhs0",
                                    "created": 1641371889269,
                                    "text": "Agdaの命題",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": [
                                    {
                                        "data": {
                                            "id": "cgxls3hnasg0",
                                            "created": 1641371904820,
                                            "text": "Agdaの型",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    }
                                ]
                            },
                            {
                                "data": {
                                    "id": "cgxlsaknc3s0",
                                    "created": 1641371920239,
                                    "text": "仕様記述の証明",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": [
                                    {
                                        "data": {
                                            "id": "cgxlshszaw00",
                                            "created": 1641371935980,
                                            "text": "Agdaの型を持つ値",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    }
                                ]
                            },
                            {
                                "data": {
                                    "id": "cgxltkpfp340",
                                    "created": 1641372020660,
                                    "text": "入力の仕様の証明を受け取る",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxltxiycpk0",
                                    "created": 1641372048566,
                                    "text": "出力の仕様の証明を次に渡す",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            }
                        ]
                    }
                ]
            },
            {
                "data": {
                    "id": "cgxlwcze89k0",
                    "created": 1641372238941,
                    "text": "実装と検証",
                    "expandState": "collapse",
                    "layout": null,
                    "font-size": 48
                },
                "children": [
                    {
                        "data": {
                            "id": "cgxlwtaxcnk0",
                            "created": 1641372274466,
                            "text": "While program",
                            "layout": null,
                            "font-size": 48
                        },
                        "children": [
                            {
                                "data": {
                                    "id": "cgxlzhv4sv40",
                                    "created": 1641372484659,
                                    "text": "for文で入力が出力に渡ることを確認",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            }
                        ]
                    },
                    {
                        "data": {
                            "id": "cgxlx190h6o0",
                            "created": 1641372291765,
                            "text": "Binary Tree",
                            "expandState": "expand",
                            "layout": null,
                            "font-size": 48
                        },
                        "children": [
                            {
                                "data": {
                                    "id": "cgxlx59xw140",
                                    "created": 1641372300528,
                                    "text": "find node",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxlx7sexjs0",
                                    "created": 1641372305999,
                                    "text": "replace node",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxlxfx8zig0",
                                    "created": 1641372323705,
                                    "text": "Invariant の変換",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            }
                        ]
                    },
                    {
                        "data": {
                            "id": "cgxlxy8w0fk0",
                            "created": 1641372363591,
                            "text": "Loop Connecter",
                            "layout": null,
                            "font-size": 48
                        },
                        "children": [
                            {
                                "data": {
                                    "id": "cgxlyewlruw0",
                                    "created": 1641372399854,
                                    "text": "Loopする際にはConnecter経由で呼び出す",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxlysjjq000",
                                    "created": 1641372429539,
                                    "text": "減少列を使用して停止性を示す",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            }
                        ]
                    }
                ]
            },
            {
                "data": {
                    "id": "cgxm0g75t5s0",
                    "created": 1641372559397,
                    "text": "Invariant",
                    "expandState": "collapse",
                    "font-family": "arial,helvetica,sans-serif",
                    "layout": null,
                    "font-size": 48
                },
                "children": [
                    {
                        "data": {
                            "id": "cgxm18bzu5k0",
                            "created": 1641372620639,
                            "text": "While program",
                            "layout": null,
                            "font-size": 48
                        },
                        "children": [
                            {
                                "data": {
                                    "id": "cgxm1fji0ko0",
                                    "created": 1641372636331,
                                    "text": "loop変数と計算結果の和",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            }
                        ]
                    },
                    {
                        "data": {
                            "id": "cgxm200laq00",
                            "created": 1641372680900,
                            "text": "Binary Tree",
                            "layout": null,
                            "font-size": 48
                        },
                        "children": [
                            {
                                "data": {
                                    "id": "cgxm24fcyyg0",
                                    "created": 1641372690500,
                                    "text": "Binary Tree の性質",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": [
                                    {
                                        "data": {
                                            "id": "cgxm2awbkfk0",
                                            "created": 1641372704586,
                                            "text": "Dataであらわしている",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    }
                                ]
                            },
                            {
                                "data": {
                                    "id": "cgxm2j23bzk0",
                                    "created": 1641372722349,
                                    "text": "Tree をたどったstack",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": [
                                    {
                                        "data": {
                                            "id": "cgxm2s45f2w0",
                                            "created": 1641372742065,
                                            "text": "Treeの減少列",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    }
                                ]
                            },
                            {
                                "data": {
                                    "id": "cgxm34s3yow0",
                                    "created": 1641372769635,
                                    "text": "replace tree",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": [
                                    {
                                        "data": {
                                            "id": "cgxm3af7vm80",
                                            "created": 1641372781916,
                                            "text": "2つのtreeが値の置き換え",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    }
                                ]
                            }
                        ]
                    },
                    {
                        "data": {
                            "id": "cgxm41iane80",
                            "created": 1641372840875,
                            "text": "DataでInvariantを表す",
                            "layout": null,
                            "font-size": 48
                        },
                        "children": [
                            {
                                "data": {
                                    "id": "cgxm4iqegso0",
                                    "created": 1641372878371,
                                    "text": "AgdaでのSet",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": [
                                    {
                                        "data": {
                                            "id": "cgxm4uktr5c0",
                                            "created": 1641372904155,
                                            "text": "Program が生成可能なData の集合全体",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    }
                                ]
                            }
                        ]
                    }
                ]
            },
            {
                "data": {
                    "id": "cgxlvb49n1c0",
                    "created": 1641372156518,
                    "text": "目標",
                    "expandState": "expand",
                    "font-family": "arial,helvetica,sans-serif",
                    "font-size": 48,
                    "layout": null
                },
                "children": [
                    {
                        "data": {
                            "id": "cgxlvdxrz4o0",
                            "created": 1641372162655,
                            "text": "xv6をGears Agdaで記述してCbCに変換",
                            "layout": null,
                            "font-size": 48
                        },
                        "children": []
                    }
                ]
            },
            {
                "data": {
                    "id": "cgxm64t605k0",
                    "created": 1641373004791,
                    "text": "発表の目次",
                    "expandState": "expand",
                    "layout": null,
                    "font-family": "arial,helvetica,sans-serif",
                    "font-size": 48
                },
                "children": [
                    {
                        "data": {
                            "id": "cgxm7egd5hk0",
                            "created": 1641373104149,
                            "text": "CbCとGears Agda",
                            "layout": null,
                            "font-size": 48,
                            "progress": 9
                        },
                        "children": []
                    },
                    {
                        "data": {
                            "id": "cgxm7tbvjz40",
                            "created": 1641373136530,
                            "text": "Meta level と normal level",
                            "layout": null,
                            "font-size": 48,
                            "progress": 9
                        },
                        "children": []
                    },
                    {
                        "data": {
                            "id": "cgxm87010zs0",
                            "created": 1641373166288,
                            "text": "実装と証明",
                            "layout": null,
                            "font-size": 48
                        },
                        "children": []
                    },
                    {
                        "data": {
                            "id": "cgxm8jn6fyw0",
                            "created": 1641373193809,
                            "text": "While Program",
                            "layout": null,
                            "font-size": 48,
                            "progress": 9
                        },
                        "children": [
                            {
                                "data": {
                                    "id": "cgxm8pumifk0",
                                    "created": 1641373207320,
                                    "text": "normal level の記述",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxm8ylm8v40",
                                    "created": 1641373226367,
                                    "text": "Hoare Conditionをつけたもの",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxm9ltb9ew0",
                                    "created": 1641373276898,
                                    "text": "test との違い",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": [
                                    {
                                        "data": {
                                            "id": "cgxm9rsei0w0",
                                            "created": 1641373289904,
                                            "text": "testでは実数をあたえる",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    },
                                    {
                                        "data": {
                                            "id": "cgxmcjx6v5s0",
                                            "created": 1641373507871,
                                            "text": "Gears Agdaでは未定義でもよい",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    }
                                ]
                            }
                        ]
                    },
                    {
                        "data": {
                            "id": "cgxm8nq0bjs0",
                            "created": 1641373202688,
                            "text": "Binary Tree",
                            "layout": null,
                            "font-size": 48
                        },
                        "children": [
                            {
                                "data": {
                                    "id": "cgxmbe451tk0",
                                    "created": 1641373416867,
                                    "text": "find node",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxmbgwimnk0",
                                    "created": 1641373422936,
                                    "text": "replace node",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxmbjnl5qw0",
                                    "created": 1641373428927,
                                    "text": "loop connecter",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxmbpi8cqg0",
                                    "created": 1641373441664,
                                    "text": "Invariant",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": [
                                    {
                                        "data": {
                                            "id": "cgxmbr88feg0",
                                            "created": 1641373445413,
                                            "text": "Binary tree",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    },
                                    {
                                        "data": {
                                            "id": "cgxmbw4mq740",
                                            "created": 1641373456079,
                                            "text": "Stack node",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    },
                                    {
                                        "data": {
                                            "id": "cgxmbybtr8o0",
                                            "created": 1641373460867,
                                            "text": "replace node",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    }
                                ]
                            }
                        ]
                    },
                    {
                        "data": {
                            "id": "cgxma4pz0ao0",
                            "created": 1641373318055,
                            "text": "将来",
                            "layout": null,
                            "font-family": "arial,helvetica,sans-serif",
                            "font-size": 48,
                            "progress": 9
                        },
                        "children": [
                            {
                                "data": {
                                    "id": "cgxmabj26zs0",
                                    "created": 1641373332875,
                                    "text": "Red Black Tree",
                                    "layout": null,
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxmagqkeww0",
                                    "created": 1641373344212,
                                    "text": "Delete",
                                    "layout": null,
                                    "font-family": "arial,helvetica,sans-serif",
                                    "font-size": 48
                                },
                                "children": []
                            },
                            {
                                "data": {
                                    "id": "cgxmajosn4g0",
                                    "created": 1641373350636,
                                    "text": "並列実行",
                                    "expandState": "expand",
                                    "layout": null,
                                    "font-family": "arial,helvetica,sans-serif",
                                    "font-size": 48
                                },
                                "children": [
                                    {
                                        "data": {
                                            "id": "cgxmap0xtvk0",
                                            "created": 1641373362254,
                                            "text": "Syncronized que",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    },
                                    {
                                        "data": {
                                            "id": "cgxmb2mfwww0",
                                            "created": 1641373391852,
                                            "text": "モデル検査との結合",
                                            "layout": null,
                                            "font-size": 48
                                        },
                                        "children": []
                                    }
                                ]
                            },
                            {
                                "data": {
                                    "id": "cgxmamno3oo0",
                                    "created": 1641373357098,
                                    "text": "xv.6",
                                    "layout": null,
                                    "font-family": "arial,helvetica,sans-serif",
                                    "font-size": 48
                                },
                                "children": []
                            }
                        ]
                    }
                ]
            }
        ]
    },
    "template": "default",
    "theme": "fresh-blue",
    "version": "1.4.43"
}