16. プログラムの静的検証、システムズプログラミングの論文 (うどん)
Update: 2018-04-30
Description
うどんくんが研究していたプログラム検証の話や、システムズプログラミングの古典的な論文についての話をしました。
出演者: うどん (@kw_udon_)、Rui Ueyama (@rui314)
ハッシュタグは#tcfmです。
TCFMはサポーターの投げ銭によって収益を上げています。このコンテンツに課金してもいいよという方はぜひクリエイター支援サイトPatreonから登録してご協力ください。
- イントロ (0:00 )
- Patreon (1:33 )
- Wikipediaに寄付するとどうなるか (2:52 )
- セキュキャン2018の講師やります (7:57 )
- プログラム検証とは何か (13:09 )
- Rustは型システムによってコンパイル時に安全性を検証できる (18:38 )
- 線形論理と線形型 (22:16 )
- 定理証明支援系Coq (26:29 )
- 関数型プログラミング言語に対するモデル検査 (39:25 )
- プログラミング言語の研究が応用されるまでには時間がかかる (44:04 )
- Misreading Chat (48:17 )
- Stanford CS240 (49:38 )
- 「悪いほうが良い」エッセイ (52:05 )
- Eraserによる動的エラー検出 (56:41 )
- 割り込みハンドラが忙しすぎてマシンがハングアップする問題を解決する論文 (1:03:23 )
- VMware ESXのメモリ管理の論文 (1:09:23 )
- MicrosoftのMidori OS (1:20:03 )
- TCFMの話題のバリエーションについて (1:21:29 )
- ガラケーを自動操作するデバイスを自作 (1:23:28 )
- セキュキャン2018
- 線形論理
- モデル検査
- 高階モデル検査
- うどんくんの出身研究室が開発している関数型プログラムの自動検証器
- プログラミング言語Rust
- カリーハワード同型対応
- Coq
- COMPCERT Cコンパイラ
- INRIA
- 四色問題
- ケプラー予想
- プログラミング言語Eiffel
- Misreading Chat
- 簡単なプログラミング言語を30分で作る実況動画
- 音の良いポッドキャストを録音するために ― Turing Complete FMの収録テクニック
- Turing Complete FMの裏側 ― Webサイト構築編
- Stanford CS240
- 「悪い方が良い」原則と僕の体験談
- Arduinoで作る携帯サイト自動巡回マシン
Comments
In Channel
Download from Google Play
Download from App Store
United States00:00
00:00
1.0x
