https://iosdiscord.connpass.com/event/82436/ での発表資料です。
理論から入門するswift/lib/Sema - わいわいswiftc #1
https://iosdiscord.connpass.com/event/82436/ での発表資料です。
「型の理論」と証明支援システム -- 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世紀の数学とコンピュ ータサイエンスの双方に、大きな影響を与え ていくだろう。
型付きラムダ計算 - Wikipedia
型付きラムダ計算（かたつきラムダけいさん、英: typed lambda calculus）とは、無名の関数の抽象表現にラムダ () というシンボルを用いる型付き形式手法である。型付きラムダ計算は基礎的なプログラミング言語でもあり、MLやHaskellなどの型付き関数型言語の基盤であり、さらには型付き命令型プログラミング言語の間接的な基盤とも言える。また、カリー・ハワード同型対応によって数理論理学と証明論とも密接に関連しており、圏論のクラスの内部言語と見なすこともできる。例えば単純な型付きラムダ計算はデカルト閉圏 (CCC) の言語である。 ある観点から見れば、型付きラムダ計算は型を持たないラムダ計算を改良したものと言えるが、別の観点からは、より根本的な理論と見ることもでき、型を持たないラムダ計算の方が型が1つしかない特殊ケースと見ることができる。 様々な型付きラムダ計算がこれまで研究され
型理論 なんて自分には関係ないと思っているあなたへ
24. ...... Lemma reduce_lemma : forall ctx (ctx' : seq (term * typ)) t ty, typing ([seq Some p.2 | p <- ctx'] ++ ctx) t ty -> Forall (fun p => reducible ctx p.1 p.2) ctx' -> reducible ctx (substitute_seq 0 [seq p.1 | p <- ctx'] t) ty. Proof. move => ctx ctx' t ty; elim: t ty ctx ctx'. - move => /= n ty ctx ctx'. rewrite /substitute_seqv typvar_seqindex subn0 size_map shiftzero. elim: ctx' n => [|
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Categories and Types in Logic, Language, and Physics
