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

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

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

• AI開発
• 入門

セッションの概要

2025年、CursorやCline、DevinなどのAIエージェントを活用した開発が主流となりつつあります。しかし、大規模な開発においては、AIが実装しやすい「枠組みの提供」と「コンテキストの最小化」が重要となります。本セッションでは、形式手法や関数型プログラミングの手法がこれらの課題にどのように寄与するかを探ります。具体的な事例を通じて、これらのアプローチがAIエージェントを活用した開発の生産性と品質向上への貢献度合いを検証していきます。

カバーするトピック

• AIエージェントを用いた開発の特徴
• 形式手法を用いた仕様モデリングと検証
• 関数型言語の代数的データ型(ADT)と関数合成の利点の活用
• 関数型DDDアプローチによる境界づけられたコンテキストごとのビジネスロジックの分離
• シフトレフトのアプローチをAI開発に適用する具体的ワークフロー

対象とする聴衆のレベル

• Beginner: 分野の前提知識を必要としない
• Intermediate: 分野の基礎知識を持っている
• Advanced: 分野に精通している
  Beginner レベルの方が楽しめる内容ですが、Intermediate、Advaced レベルの方には内容へのツッコミを楽しんでもらえる内容になると思います。

セッションのテーマ

• Tips
• 入門

セッションの概要

計算機プログラムは現実のフォン・ノイマン型計算機上での計算が前提ですから、命令を記述する部分が必ずあります。
I/Oがその典型です。このセッションでは、そのI/O部分をできるだけ、小さく一箇所に隔離する方法を対話的ソート問題を例に紹介します。

• 命令的Haskellプログラミング vs 関数的Haskellプログラミング
• プレリュード関数 interact :: (String -> String) -> IO () の紹介
• インタラクティブ・ソートの実装

対象とする聴衆のレベル

• Intermediate
  • Scala 製の非同期ランタイムである Cats Effect 3 の実装に沿った話をしますが、概念レベルの話がメインになるため、Scala そのものの前提知識は仮定しません
  • ただし、（トーク内で説明はするものの、）ラムダ計算がどのようなものなのか、という点と、β簡約の計算方法をある程度把握していることは想定します

セッションのテーマ

• 言語処理系（インタープリター）
• 理論
• 非同期ランタイム

セッションの概要

単一のプロセスで並行処理を行う方法として、OSカーネル上でスレッドを大量に作成する代わりに、細切れにした「タスク」をユーザーランドで処理し続ける、いわゆる非同期ランタイムが使われることが増えてきています（例: goroutine、tokio-rs、Cats Effect、Project Loom）。アプリケーション内部に用意したスケジューラを用いて実行するタスクを切り替えていくこれらの機構は、使い方こそスレッドベースの非同期プログラミングと大差ない（場合によっては、同期プログラミングとも大差ない）ものの、そのランタイム実装まで追ったことのある方は多くないのではないでしょうか。

この講演の前半部分では、ラムダ計算から出発して、ラムダ計算のシンプルな「インタプリタ」であるCEK 機械の仕組みと動作について詳しく解説します。そして後半部分では、CEK 機械の仕組みを通して、非同期ランタイムの実装（の一パターン、特に Cats Effect 3 の実装）を理解できるのだと道案内することを目標とします。

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

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

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

• 導入事例

セッションの概要

マイクロサービス内で動いているAPIをF#で書いて運用を2年ほど続けて得られた知見をお話します。
Domain Modeling Made Functionalが翻訳されたのをきっかけにF#という言語に興味をもたれた方も多いと思いますが、実業務でF#を採用しているという話は珍しいと思うので以下の観点についてお話できたらと考えています。

• F#でWeb APIをどのように開発するのか
• どのように設計するのか
• 実運用において困ることはあるのか
• どういう課題があるのか

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

• Beginner: 分野の前提知識を必要としない
• Intermediate: 分野の基礎知識を持っている

セッションのテーマ

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

セッションの概要

Elmは型安全性や開発体験の良さが注目されがちですが、実際のパフォーマンスはどうなのでしょうか？
「Elmは遅いのか？速いのか？」という疑問に対して、実際にベンチマークを取り、得られた知見を共有します。
処理が重いサンプルコードを起点に少しずつ改良を進め、パフォーマンスを向上させてみましょう。

• 1万行のCSVをデコード＆前処理するサンプルコード
• elm-benchmarkを使ってパフォーマンスを測定してみよう
• List を Array に置き換えると、どのくらい速くなる？
• 本当のボトルネックを探して改善する
• CSVではなく、JSONのデコードにしてみると...？
• ベンチマークで得られたもの

対象とする聴衆のレベル

• 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#でこのブログを構築した」に綴っています。セッション内で語りきれなかったテーマについても、懇親会などでぜひお話ししましょう！

対象とする聴衆のレベル

• 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: 分野の前提知識を必要としない（コンパイラ構成について）
• Intermediate: 分野の基礎知識を持っている（関数型言語の使い方について）

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

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

セッションの概要

SML#は、Standard MLを包摂する、純国産のフルスケール関数型言語です。本セッションでは、SML#のコア開発者のひとりが、関数型言語とそのコンパイラを開発する者の視点で、関数型言語を作る上での苦悩と工夫をお話しします。

いくら理論が美しかろうと、言語が高機能だろうと、現実に使えなければ絵に描いた餅です。現実に使えるかどうかの判断基準のひとつは、CPUやメモリなどの計算資源の利用効率の高さ、有体に言えば「速さ」でしょう。ラムダ計算に端を発する関数型言語は、今日主流の命令的な計算機アーキテクチャとは計算モデルから異なるため、現実の計算機を効率よく駆動するネイティブコードを出力する関数型言語コンパイラを開発するのは自明なことではありません。その困難を、ときには新たな理論を開発して、ときには力技で乗り越え、今日の関数型言語コンパイラが成立しています。

コンパイル結果のコード（ひいてはコンパイラそのもの）を速くするには、「CPUコアを増やす」「速いCPUを使う」「コードの無駄を省く」の3つのアプローチが考えられます。最新のSML#コンパイラは、これらのアプローチそれぞれについて、「タスク並列を実現するためのガベージコレクション」「ARM対応のための末尾呼び出しコンパイル」「自然意味論に基づく部分評価器」を装備しています。本セッションでは、SML#コンパイラ全体のアーキテクチャを俯瞰しつつ，これらコンパイラの機能の開発経緯とその理論・技術に焦点を当てます。

本セッションに参加することで、「SML#の使い方」だけでなく「SML#の作られ方」もなんとなくわかった気になる、また関数型言語の裏にあるバイナリな部分にも目が向くようになる、そんな発表を目指します。

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

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

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

• 入門
• オブジェクト指向プログラミング

セッションの概要

このセッションでは、オブジェクト指向型プログラミングの中に関数型プログラミングの考え方を取り込む方法を、「スタティックおじさん」との対話を通じて学びます。

近年、オブジェクト指向プログラミングの中に関数型プログラミングの要素を取り入れる手法が注目されています。
私もプロジェクトや趣味のプログラミングの中で、可能な範囲でこの考え方を活かそうとしています。

しかし、そんなときに立ちはだかるのが「スタティックおじさん」です。
「副作用を減らすなら static を使えばいいのでは？」
「関数型って、要するにスタティックメソッドをたくさん使うこと？」
これらの疑問、実は多くの人が抱くものではないでしょうか。

本セッションでは、

• スタティックメソッドと関数型の考え方の違い
• オブジェクト指向の文脈で関数型を適用する具体的な手法
  • 「スタティックおじさん的思考」から脱却して、関数型の本質を踏まえた設計をする方法
    をストーリー仕立てで学んでいきます

「スタティックおじさん」と一緒に、オブジェクト指向における関数型プログラミングへの第一歩を踏み出しましょう！

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

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

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

• 導入事例

セッションの概要

概要

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

認証フローの状態遷移

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

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

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

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

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

対象

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

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

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

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

• ライブラリやフレームワーク
• 言語処理系（コンパイラー、インタープリターなど）
• 理論
• 入門
• tagless-final

セッションの概要

ソフトウェア開発において、複雑なビジネスドメインを正確に捉えることは極めて重要です。しかし、その過程でしばしば直面するのが、余計な詳細や偶有的複雑さ（accidental complexity）です。これらはシステムを理解しにくくし、保守コストを高める原因となります。
そこで鍵となるのが「抽象」の役割です。本発表ではドメインモデリングにおける抽象の役割を取り上げ、問題空間と解決空間の橋渡しや、ドメインの核となるモデルを的確に表現する土台を作り上げることの重要性について述べます。そして、これらを実現するためのアプローチとして、tagless-finalによる型安全なDSL構築手法について取り扱います。さらに、DSL自体を、型安全に最適化あるいは拡張していくための方法について扱います。また、ソフトウェア開発において、DSLをいつ作るべきか、どのように活用するか、についても触れます。

キーワード：

• DDD（ドメイン駆動開発）、ドメインモデリング
• DSL（ドメイン特化言語）
• 抽象
• tagless-final、高階抽象構文
• プログラム変換と最適化
• 部分評価（partial evaluation）
• Normalization by Evaluation（NbE）
• 開発生産性と品質
• Software Product Line（SPL）

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

• Beginner: 分野の前提知識を必要としない
• Intermediate: 分野の基礎知識を持っている

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

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

セッションの概要

「関数型まつり」のWebサイトを構築するにあたり、 elm-pages というフレームワークを採用しました。
本発表では、elm-pagesの特徴や採用の理由、実際の開発プロセスを紹介しつつ、Elmを用いた静的サイト開発のメリット・課題について考察します。

• elm-pagesとは？ 他の静的サイトジェネレーターなどとの比較
• 関数型まつりWebサイトでの適用事例
  • 選定理由と導入の流れ
  • 開発時の工夫やハマりどころ
• Elmで静的サイトを作るメリットと課題
  • 型安全なデータ管理とバグの少なさ など
  • 実運用における課題

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

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

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

• 入門
• C#（LINQ）
• Java（Steram API）

セッションの概要

このセッションでは、C#やJavaを事例として、手続き型構造化プログラミングから関数型プログラミングへの移行と、これらを混在させた環境でのコードの読み方/書き方を解説します。

• 新しいプロジェクトで関数型プログラミングが導入されたけれども、なんだかなじまない
• 関数型に慣れない人が、つい手続き型の書き方をしてしまう
• もっとうまく関数型プログラミングを扱いたいけど、どうしたらいいかわからない
  こんな経験はありませんか？

私はこの違和感を「気持ち悪さ」として捉えていました。それはどこから来るのでしょうか？
現代の多くのプログラマーは、手続き型構造化プログラミングで学習し、キャリアを築いています。
その習慣のまま関数型プログラミングに取り組もうとすると、適切なコーディングができなかったり、意図しない形で手続き型のパターンを持ち込んでしまったりします。

特に、C#やJavaのようなオブジェクト指向言語に関数型の概念を取り入れた場合、この違和感はより顕著になります。
手続き型の思考と関数型の考え方のギャップを整理し、どのように適応すれば「気持ち悪さ」から脱却できるのかを解説します。

対象とする聴衆のレベル

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

セッションのテーマ

• ライブラリやフレームワーク

セッションの概要

広域分散環境で実行したいとき自分でお膳立てするのはなかなか大変です。
このセッションではElixirの実行を広域分散環境で実行するフレームワーク、FlameとGiocciの2つを紹介します。Flameは、通常ローカルマシンで実行されるElixirの関数実行を、fly.ioなどのクラウドへ飛ばして実行するフレームワークです。Giocciも同様に外の計算エンティティに関数実行を飛ばしますが、Flameと違って実行先を決め打ちしなくても複数の計算エンティティで実行が可能です。
今回はElixirを例に話しますが、おそらく他の関数型言語にも同様の機能があったり、作るとしてもそれほど難しくないと思いますので、みなさんと情報共有して関数型言語の世界を広げていければなと思ってます。

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

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

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

• 導入事例
• Tips

セッションの概要

Siiibo証券株式会社は2019年に創業して以来、バックエンドにElixir，フロントエンドにElmと関数型言語をフルスタックに採用して、社債専門の証券システムを作り上げてきました。
このセッションでは実際に関数型言語を業務で（特にスタートアップ企業などの少人数開発組織で）採用し、維持し、継続するにあたって重視している価値観、手続き、手法などをざっくばらんに紹介してみようと思います。

• 狂気
• コードレビュー/CI/Upkeep
• ビルドとテストの高速化
• 静的型付けでない言語だからといって型のことを考えないわけじゃないし、型はほしいし、願えば型は降ってくるかもしれない
• 情報収集/コミュニティ参画
• 新しい手法を取り入れる
• 覚悟

対象とする聴衆のレベル

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

セッションのテーマ

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

セッションの概要

Scala は関数型プログラミングとオブジェクト指向プログラミングのパラダイムを併せ持つ言語です。JVM 上で動作し、Java のエコシステムを活用できるため、業務アプリケーションにも多く採用されています。

本セッションでは、強固な型システムで作られた Scala の関数型ライブラリを活用し、Web アプリケーションを開発する方法を紹介します。業務アプリケーションの実例を交えながら、ドメインモデルやドメインロジック、Web API の型安全な記述方法についてお話します。主に以下の内容を含みます。

• Refinement Types
• Opaque Type
• Union Type
• Tagless Final

型を活用することで、データの整合性を静的に保証し、エフェクト管理を型安全に実装しながら、疎結合な設計を維持できます。本セッションでは、それらの具体的な適用例や、関数型のアプローチがどのように業務開発に役立つのかを、実践的な観点から解説します。

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

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

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

• 理論
• Tips
• 入門

セッションの概要

静的な型付けを行う言語において、関数の制約を表現する方向性は二つあります。

一つは戻り値で制約を表現する方向

def max[A: Ordering](list: List[A]): Option[A]

もう一つは引数で制約を表現する方向

def max[A: Ordering](list: NonEmptyList[A]): A

このセッションでは、それぞれの違いについて認識するための型の Cardinality という概念を紹介します。
また、具体のシステムにおいてそれぞれの選択がどういった影響を及ぼすかを紹介し、普段のプログラミングにおいてどういったケースでどちらを選択したらよいかの指針を示します。

対象とする聴衆のレベル

• Beginner: 分野の前提知識を必要としない
• Intermediate: 分野の基礎知識を持っている

セッションのテーマ

• 理論
• 入門

セッションの概要

本セッションでは、プログラミング言語の標準化を、人間が話す言語における「標準語」「言語規範」と類比させ、社会言語学的視点から考察します。具体的には、Haskell・ANSI C・JavaScript (ECMA-262) という 3 つのプログラミング言語の標準化プロセスを取り上げ、それぞれが「複数の実装・方言が先に存在し、それらをまとめるために標準化を行った」という共通点を持つことに着目します。

Haskell は当時数多くの非正格な純粋関数型プログラミング言語が乱立していた状況を収斂させるために、ANSI C は初期の多様な処理系を政治的にまとめて権威ある承認 (imprimatur) を得るために、そして JavaScript (ECMA-262) は本来の意図を超えてブラウザ間の実装の差に留まらない範囲にまで活用範囲が拡張していったという混沌を統治するために、いずれも大きな労力と妥協を経て標準化されました。
ところで、一旦規格が制定されてしまうと、世の中に「正しい処理系」と「正しくない処理系」が誕生してしまうことになります。今までは「まあ、こんな感じに動くものがこのプログラミング言語だよね」だったのが、規格化以降は「この処理系は正しい」「この処理系は規格非準拠であり、誤っている」という価値観に晒されることになってしまいます。
人間が用いる言語においては、こういった「標準語の威信 (prestige)」というテーマは、社会言語学という分野において頻繁に取り上げられる定番のテーマとなっています。本セッションでは、プログラミング言語の標準化プロセスおよびその後のプログラミング言語コミュニティに対してこういった論じ方を試み、プログラミング言語の標準化がどのような社会的・文化的背景を持っているのか、その過程で生まれた数多くの、よく「歴史的経緯」という言葉で十把一絡げで扱われる事象について、より深く理解することを目指します。

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

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

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

• 入門
• 理論

セッションの概要

本セッションでは、プログラミングにおける再帰の基礎を初心者向けにわかりやすく解説します。まず、再帰とは何か、そしてなぜ関数プログラミングにおいて重要なのかを説明し、簡単な例を通じてその概念を掴んでいただきます。また、命令型プログラミングにおけるループ処理と、関数プログラミングにおける再帰アプローチの違いについても、実際のコード例を用いて比較し、解説します。

さらに、再帰を利用する際に直面しがちな問題点とその対策にも触れます。例えば、再帰呼び出しが深くなりすぎることで生じるスタックオーバーフローなどのリスクについて説明し、それを回避するテクニックとして末尾呼び出し最適化を紹介します。また、より高度な話題として継続渡しスタイルによる再帰の書き換えにも触れ、パフォーマンスやスタック使用量の観点から再帰を最適化する方法を概観します。

その後、再帰の実践的な応用例として、木構造の探索アルゴリズムやファイルシステムの再帰的な探索処理を紹介します。これらの例を通じて、再帰が現実世界の問題解決にどのように役立つかを具体的に示します。

初心者の方でも安心して参加できる内容となっており、再帰の基礎から応用までを学べるセッションです。

Duplicate: https://fortee.jp/2025fp-matsuri/proposal/e0274da9-d863-47fe-a945-42eb04185bb9

操作ミスで同じプロポーザルを2回提出してしまいました。すみません……