Turing Complete Fm

うどんくんが研究していたプログラム検証の話や、システムズプログラミングの古典的な論文についての話をしました。出演者: うどん (@kw_udon_)、Rui Ueyama (@rui314) https://turingcomplete.fm/16 ハッシュタグは#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 「悪い方が良い」原則と僕の体