対象とする聴衆のレベル

• Intermediate: 分野の基礎知識を持っている

セッションのテーマ

• 言語処理系（コンパイラー、インタープリターなど）
• Tips

セッションの概要

型システムはある種のバグを静的に検査可能な手法で、多くの型システムは健全性を満たします。つまり、型システムが言うことは全て正しいです。

一方で、実世界の型システムは、ひょんなことから健全性を破壊する「穴」が存在していたりします。怖いですね。
本トークでは、Java や Rust、OCaml など、実世界のプログラミング言語における型システムの「穴」を概観します。罠を事前に知ることで、実際にハマったときの素早い対処や、プログラミング言語への深い理解が期待されます。

対象とする聴衆のレベル

• Intermediate: 分野の基礎知識を持っている

セッションのテーマ

• 導入事例
• 理論

セッションの概要

本セッションでは、AWS によって定理証明支援系 Lean を用いて開発されたポリシー記述言語 Cedar について、定理証明の役割や実サービスとの接続に焦点を当てて解説します。

Web サービスのセキュリティを考える上で、権限管理の設計は不可欠です。Cedar は AWS の IAM と同様、許可ルールと拒否ルールを組み合わせてポリシーを定義することで、リクエストに応じて許可もしくは拒否を返します。また、カスタム型を含むスキーマ定義が可能で、型検査も行われます。Cedar は OSS として公開されている他、マネージドサービスが Amazon Verified Permissions として利用可能です。

Cedar 開発の鍵のひとつとなったのが、定理証明支援系 Lean です。Cedar には操作的意味論が定義されており、「ポリシーの評価は必ず停止する」「拒否ルールは許可ルールに優先する」といった認可エンジンとしての仕様や、型システムの健全性について Lean で証明が行われています。また、認可エンジンとしてのスケーラビリティを実現するために、Cedar はポリシー内で判定に関係する部分のみを抽出する slice と呼ばれる最適化を実装しており、その健全性も Lean により証明されています。

もう一つのポイントは定理証明から実装への接続です。多くの定理証明支援系では実行可能なプログラムの抽出が可能ですが、実システムへの適用ではパフォーマンスやエコシステムが課題となりがちです。このギャップを乗り越えるため、Cedar では認可エンジン自体は Rust で開発し、Rust による実装と Lean による証明済み実装の両方に同じランダム入力を与えて出力の一致を確認する手法が採用されています。

Cedar は、定理証明が AWS という巨大システムの中で活用されている点で非常に特徴的なプロダクトです。本セッションでは、このような実世界との接続について、論文、OSS 実装、そしてサービス化された機能をそれぞれ参照しつつ解説します。

対象とする聴衆のレベル（該当するレベルを記載してください。）

• Beginner: 分野の前提知識を必要としない

セッションのテーマ（該当するテーマを記載してください。なければ追加頂いて良いです）

• 入門
• 周辺ツール（ビルドツール、静的解析ツール、エディターなど）
• 言語処理系（コンパイラー、インタープリターなど）

セッションの概要

LISPは記号処理に特化して初期の人工知能研究を牽引した言語であり、実用的な関数プログラミングを提供した最初の言語といえるでしょう。
現在のLisp族の末裔たちも関数プログラミングのための機能を備えている一方、後続の関数型言語(ML族)が持つ静的型や参照透過性、モナドなどの機能は持っていません。

このトークでは日常的にEmacsとEmacs Lispを利用しているユーザーが、Lispのどのような側面が「関数型」的で、なぜ関数型言語ではないと考えているのか、Emacsを用いたプログラミングの実践とEmacs Lispの「正体」までお話しします。

対象とする聴衆のレベル（該当するレベルを記載してください。）

• Beginner: 分野の前提知識を必要としない

セッションのテーマ（該当するテーマを記載してください。なければ追加頂いて良いです）

• 導入事例

セッションの概要

概要

医療業界向けに複数のSaaSプロダクトを提供するコンパウンドスタートアップ「カケハシ」では、OIDC (OpenID Connect) 対応の共通認証基盤を開発・運用中です。OIDC対応の認証基盤の開発では、画面をまたぎながら多様なパラメータを取り扱うため、不正な状態遷移やバリデーション漏れが大きなセキュリティリスクとなります。本セッションでは、TypeScriptで代数的データ型 (Algebraic Data Types; ADT) を活用し、以下のような特徴的なポイントを押さえて実装した事例を紹介します。

認証フローの状態遷移

OIDCを利用した認証フローでは、多数のパラメータを扱う複雑なバリデーションが要求されるうえ、アカウント選択→認証→同意といったステップを画面遷移を伴いながら進める必要があるため、状態管理も非常に煩雑になります。

そこで、 「アカウント選択済み」「認証中」「同意完了」など、認証フローの状態と振る舞いを代数的データ型で表現します。これにより、型システムを活用して不正な状態遷移（例: 同意せずに認証を終了、画面Aをスキップして画面Bに直行してしまう）を排除できます。

バリデーション漏れの防止

代数的データ型は、バリデーション漏れの防止にも有効です。様々なユースケースで利用できるように設計されたOIDCでは、数多くのパラメータをバリデーションする必要があります。

そこで、バリデーションの状態を代数的データ型で表現することで、不正なパラメータが渡されることを防止します。

対象

• TypeScriptや関数型ドメインモデリングに興味のあるエンジニア
• OIDC対応の認証フローを安全に実装したい開発者
• 表現力の高い型システムをセキュリティ向上に活かしたい方

対象とする聴衆のレベル（該当するレベルを記載してください。）

• Intermediate: 分野の基礎知識を持っている

セッションのテーマ（該当するテーマを記載してください。なければ追加頂いて良いです）

• Tips

セッションの概要

Coqには、証明付きプログラミングを容易にする Program 機構があります。本LTでは、この Program 機構の概要とその利用例を紹介します。

この機能を紹介する題材として、インデックスを用いたリストの要素取得を取り上げます。Coq において、指定したインデックスにあるリストの要素を取得する場合、通常は option 型を返すか、指定したインデックスに要素がない場合に備えて、あらかじめデフォルト値を渡す必要があります。しかし、指定したインデックスがリストの長さ未満ならば、毎回 Some が返ってくることは明らかです。

本LTでは、Program 機構を活用し、インデックスがリストの長さ未満であることが前提の場合に、option 型を用いず、またデフォルト値を与えることなくリストの要素を取得できることを紹介します。「Coqにこんな機能があるのか！」と興味を持ってもらえたら幸いです。

対象とする聴衆のレベル（該当するレベルを記載してください。）

• Beginner: 分野の前提知識を必要としない

セッションのテーマ（該当するテーマを記載してください。なければ追加頂いて良いです）

• 理論
• 入門

セッションの概要

関数型プログラミングと聞いて、初心者の方が一番に連想するキーワードは"純粋関数"ではないでしょうか。
一方で、純粋関数を作るうえで"副作用を受けない・スコープが決まっている値"というのは非常に重要ですが、この概念=代数的データ型についてはまだそれほど広まっていないように思います(主観)

そこで、このセッションではKotlinを用いて直積型と直和型から始まり、enumとSealed classとの違いについてまでお話しします。

対象とする聴衆のレベル

• Beginner: 分野の前提知識を必要としない

セッションのテーマ

• 導入事例
• ライブラリやフレームワーク

セッションの概要

私のブログサイト https://blog.pizzacat83.com を作るために F# でジェネレータを実装した話です。このブログサイトはFornaxという静的サイトジェネレータをforkしたジェネレータで生成しています。

Fornaxは、データの読み込みやサイトの生成処理を F#スクリプトで書くと、それを実行してサイトを生成してくれる、というものです。これにより、以下のメリットがもたらされます。

• テンプレート言語の表現力の制約に縛られず、F#で実装すればなんでもできる
• 一般的なテンプレート言語と違い、F#譲りの型検査・コード補完等が使える

データ読み込みやサイト生成をF#スクリプトで表現するからこそ、データソースとしてファイルから読み込むことも、headless CMSのAPIを叩くこともできます。サイト生成処理の中ではMarkdownをHTMLに変換することも、Markdown一式からRSSを生成することも、自在に実装できます。そしてこれらの処理をすべて F#で実装するので、F#の型システムの恩恵を存分に享受できます。補完のないままテンプレート言語を書いて実行時エラーに悩まされる必要はないのです。

セッションでは以下について話す予定です。

• Fornaxの魅力
• Fornax内部の仕組み
  • F#スクリプトを実行時に読み込んで、Fornax自体とスクリプトの間でオブジェクトをやり取りするには？
  • ファイルをウォッチして、変更があった場合にサイトを再生成してブラウザをリロードするには？

なお、Fornaxの使い方や私がFornaxを選定した背景などは、ブログ記事「F#でこのブログを構築した」に綴っています。セッション内で語りきれなかったテーマについても、懇親会などでぜひお話ししましょう！