D-7 07/27 16:00 ～ 16:40
サーバーレスアーキテクチャの数理的理解と分析

サーバーレスアーキテクチャは強力ですが、同時に冪等性やトランザクションなど特有の考慮事項が必要であり、高い設計力が求められます。ところで、安全なプログラムを書く上で、静的型付き言語は広く利用されていますね。型はいわば実行前に間違いを検出できる仕組みであり、その背後には「プログラムの正しさ」を厳密な数式で記述し分析する理論が存在します。では、同様に「サーバーレスの正しさ」も厳密な数式で記述することは可能でしょうか？本講演ではAWS Lambdaを用いた設計を例として取り上げながら解説します。

Ask the Speaker（Q&Aコーナー）を実施する場合は、記載しているセッション終了時間頃より5分程度、同じ配信ページ上で行います。

チェシャ猫[ProofCafe]

ProofCafe
Software Engineer

普段の業務では、DockerやKubernetesを中心としたコンテナオーケストレーションやサーバーレス技術の検証と基盤設計を担当。それと並行してプライベートでは、関数型プログラミングや形式手法によるソフトウェア検証について研究していたりいなかったりする。またコミュニティ活動として、クラウドネイティブと形式手法との交点を模索しつつ、各方面の勉強会やイベントにて登壇を行う。トレードマークは猫耳。