[B! Coq] KatagiriSoのブックマーク

Coqと少しの圏論が分かる人向けのhomotopy type theory(その1) -

The HoTT Book http://homotopytypetheory.org/book/ が完成したらしいけど、どっちかというと、数学者向けに書かれてて500ページもある。homotopy type theoryで今できてることって、CoqやAgdaで書いたら、せいぜい数千行とか、そんなもんじゃないかと思うので、長すぎる気がする一応、HoTTに関わる知識は、型理論の他に、ホモトピー論や圏論(モナドとかHaskell関連で出てくる類の知識はあまり知らなくてもいいけど、higher categoryとか教科書に書いてなさそうな話題や、モデル圏とかを知ってるといい)があって、全部真面目に勉強しようと思うと、それぞれのテーマで一冊以上の本が書ける。ただ、実際には、ホモトピー論や圏論はアイデアや視点を提供しているだけで、あくまでCoqやAgdaで書かれてる部分が重要なので、ホモトピー論や

KatagiriSo 2016/07/05

リンク

「型の理論」と証明支援システム -- COQの世界

2. Agenda     はじめに Part I : 「型の理論」をふりかえる Part II : Curry-Howard対応について Part III: Coq入門 3. はじめに  現在、HoTT(Homotopy Type Theory)と呼ばれる新しい型の理論とそれを基礎付ける Univalent Theoryと呼ばれる新しい数学理論が、熱い関心を集めている。  Univalent Theoryは、数学者のVladimir Voevodskyが、論理学者Per Martin-Löfの型の理論を「再発見」したことに始まる。  この新しい分野は、21世紀の数学とコンピュータサイエンスの双方に、大きな影響を与えていくだろう。

KatagiriSo 2016/07/05

リンク

IIJ Research Laboratory

ネットワークの計測と解析インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行うために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ 技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで