タグ

ブックマーク / ie.u-ryukyu.ac.jp/~kono (4)

  • Compiler Construction の授業

    Compiler Construction の授業 コンパイラとは何か 実行系のArchitecture Intel64 のアセンブラ 字句解析、構文解析、コード生成 部分計算と中間木 yaccによる構文解析 llvmを使ったコンパイル Micro-C の全体構成 コード生成の詳細 共通部分式 さらに進んだコンパイラ技術 参考書 Compilers: Pearson New International Edition: Principles, Techniques, and Tools More information: 今後の授業の予定 TL/1 小さいコンパイラの例題 repository レポートは、「Report on Compiler Construction Lecture Exercise 6.1 」という 形式のSubjectで メールでkono@ie.u-ryukyu.a

  • Agda による圏論入門

    Menu Menu Agda で証明しながら圏論を学ぶという予定です。あまり入門ではないかも。 Higher-Order Categorical Logic の 0章に相等する内容です。 BitBucket category-exercise-in-agda source code Agda の入門の要約 Agda の入門 Agda の集合の Level Agda の record Agda のReasoning Caategory module と圏の入門 自然変換 IdentityFunctor と Hom Reasoning Monad の結合則 Sets と Monoid を使った Monad の例 Kleisli 圏の構成 ここまでが Monad を理解するための部分。以下は、Adjoint 関連です。 Adjoint から Monad を導く Kleisli 圏による Mona

  • Software Engineering Lecture s07

    Menu Menu Monad の組み合わせ 今日の元ネタはここ。 http://www.slideshare.net/tanakh/monad-tutorial これと、 http://d.hatena.ne.jp/m-hiyama/20070507/1178496486 これ。 T1 という Monad を作ったのは良いが、これと、IO Monad は一緒に使えるのか。使うにはどうすれば良いのか? Monad M と Monad N があったとする。この合成 Monad MN は、どうすれば作れるのか? M : A -> A, N : A -> A の Functor なので、T = MN とすれば良さそうである。 ηm : 1->M μm : MM->M ηn : 1->N μn : NN->N これから、 μt : 1->T ηt : TT->T ができれば良い。ηt は、 ηt

    hiroyukim
    hiroyukim 2013/07/22
  • ソフトウェア工学

    Menu Menu この授業では、Haskell と Agda を使って、ソフトウェアの信頼性を高める手法の一つである証明について学びます。 参考書 「やさしい Haskell 入門 (バージョン98)」 すごい Haskell Miran Lipova 達人プログラマー アンドリュー ハント、デビッド トーマス (ピアソン・エデュケーション) オブジェクト指向における再利用のためのデザインパターンエリッ ク ガンマ (著), ラルフ ジョンソン (著), リチャード ヘルム ( 著), ジョン ブリシディース (著), Erich Gamma (原著), Ralph Johnson (原著), Richard Helm (原著), John Vlissides (原著), 位田 真一 (翻訳), 吉田 和樹 (翻訳) プログラミング作法 ブライアン カーニハン (著), ロブ パイク

    hiroyukim
    hiroyukim 2013/07/02
  • 1