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

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

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

• 入門
• 理論

セッションの概要

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

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

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

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

対象とする聴衆のレベル

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

セッションのテーマ

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

セッションの概要

「ElixirでIoT!!」と Erlang & Elixir Fest 2019 で喧伝しだしてから早くも５年以上の月日が流れてきました．
提案者はこれまで，「ElixirはIoT向きのプログラミング言語である」という旗印のもとで，IoTシステムに使える(はずの)さまざまなライブラリやプラットフォームをElixirで作ってきて，そしてそれらの価値を指し示すための「論よりRUN!!」なデモをお見せしてきました．
今回の発表では，どのような技術的思考と願望からこのような活動を進めてきたのか，そして得られてきた研究開発の成果を振り返りたいと思っています．
そして，提案者は正直に申し上げると，関数型言語はElixirしか分かっていません．参加される皆さまそれぞれに思い思いの「推し」があるはずですので，それらもIoT開発に使えるのか？使うとしたらどういう素敵なことが起きるのか？ざっくばらんに語り合えたらと考えています．

• マクラ：IoTシステムとは？広域分散とは？
• なぜ「ElixirでIoT!!」なのか？
  • アクターモデル由来の疎結合アーキテクチャ
  • Erlang/OTP由来の軽量かつ堅牢な並行プロセスモデル
  • そして言語機能と完全互換なNervesプラットフォーム
• これまで作ってきたものと「論よりRUN!!」
  • Rclex: Elixirエコシステムと連携するロボットシステム向けAPIライブラリ
  • Zenohex: クラウド／エッジ連携に柔軟な通信プロトコルZenohのAPIライブラリ
  • Giocci: 広域分散システム向けの資源透過型計算プラットフォーム
• 「〇〇でIoT!!」はあなたの関数型言語で成立するのか？？

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

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

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

• 理論

セッションの概要

昨今巷で Effect システムが流行っていますが、実はその双対、Coeffect システムというものがあるのをご存じでしょうか。
Effect が関数のボディでの作用について述べるシステムだとすれば、Coeffect は対称的に、引数の性質について述べるシステムです。変数の使用回数のトラッキング、セキュリティレベルの追跡などがそのインスタンスになることが知られています。

Effect システムについても軽く説明しますが、型付きラムダ計算等の知識は前提とします。

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

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

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

• 導入事例

セッションの概要

関数型言語の応用例として、制御をElixirで行った小水力発電所の例を紹介します。現在の産業機械の制御に使われてるハードウェア・ソフトウェアは多くの問題を抱えており、それを近代化する手法の一つにElixirの導入があると考えています。セッションではおおよそ以下の話をする予定です。

1. 産業システム制御における課題点
2. 小水力発電所の解説
3. 小水力発電でElixirを使う判断をした経緯
4. 産業でElixirを使うためにハードウェアを開発した話
5. 実際の応用例
   このセッションで実社会における現実の課題にどのように関数型言語を役立てていけるかの議論ができると嬉しいです。

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

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

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

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

セッションの概要

高階関数を用いたI/Oの実現方法について、TypeScriptでの例をご紹介します。

関数型プログラミングでは、高階関数や部分適用を活用することで、DIコンテナに依存することなくI/Oを実現することができます。
私の周りでは、オブジェクト指向プログラミングやそのフレームワークに慣れ親しんだプログラマーが関数型プログラミングを学び始める際に、
以下のような戸惑いを感じるケースを見てきました。

• DIコンテナ無しで依存関係をどのように解決するのか分からない
• 関数型のアプローチにはDIコンテナを置き換える手段が存在しないように感じられる

私自身も関数型プログラミングを学び始めた当初は、同様の戸惑いを感じていました。
オブジェクト指向プログラミングでは、フレームワークが提供するDIコンテナを使うことは一般的です。
これに慣れていると関数型プログラミングでの設計にギャップを感じることがあります。

私は関数型プログラミングが楽しいですし、実用性も感じています。もっと広まってほしいと願っています。
しかし、上記のような理由で、関数型プログラミングの学習に躓いたりすることもあると思います。

今回のトーク内容としては、以下のような内容を予定しています。

• 高階関数と部分適用の説明
• 高階関数を使ったI/Oの例やテストの書き方
• 実際のWebアプリケーションでの適用例

高階関数や部分適用は実用的なテーマですし、I/Oの実現方法についても関数型プログラミングの魅力の一つだと感じます。
このセッションを通じ、より実用的な関数型プログラミングの知識を共有できると嬉しいです。

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

• Intermediate: 分野の基礎知識を持っている
• Advanced: 分野に精通している

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

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

セッションの概要

本発表では、関数型プログラミングにおいて最も強力な概念の一つである、残りの計算を表す"継続"とその進化について、歴史的背景から最新技術までを包括的に整理します。
アセンブリレベルのコントロールフローやC言語のgotoといった低水準の制御命令から、構造化プログラミング期における明確な制御構造の発展、そしてSchemeにおけるcall/ccなどの継続演算子の登場へと、歴史を辿っていきます。さらに、CPS変換やANF、CFGとの対応を通じ、言語処理系の中間言語としての継続の性質について考察します。
加えて、async/awaitやモナド、代数的効果といった近年発展を続けている副作用の管理方法や、ワンショット性を考慮した効率的な実装など、先進的な概念･技法について論じ、継続が言語設計および実装に与える影響と今後の可能性を探ります。

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

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

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

• 理論
• Tips
• 入門

セッションの概要

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

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

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

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

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

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

Leanで正規表現エンジンをつくる。そして正しさを証明する

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

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

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

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

セッションの概要

このセッションでは、Leanの二面性—定理証明支援系としての強力な検証能力と、依存型を備えた純粋関数型プログラミング言語としての実践性—を活かし、正規表現エンジンの実装とその正しさの検証に取り組んだ経験を紹介します。

Leanが純粋関数型言語として持つ特徴を紹介し、特に配列に対する破壊的変更（！）のサポートに注目します。この仕組みを活かすことで、オートマトンベースの正規表現エンジンを効率的に実装できることを説明します。

次に、正規表現エンジンの実装の正しさを検証する過程で直面した具体的な課題、たとえば正規表現の仕様自体の曖昧さや証明の再利用をどのように解決したかを実例を交えて掘り下げます。通常のソフトウェア開発のようにモジュール化で対処したケースもあれば、定理証明支援系ならではの問題とその解決法など、さまざまな例を紹介します。

その他にも、依存型の利用についてもお話しします。依存型は型システムの強力さを一段引き上げますが、一方で型システムに対して人工的な制限も追加してしまいます。ある意味で諸刃の剣である依存型に対して、どのような場面で使うのが良いのか、どのような場面では避けた方が良いのかを例を挙げて説明します。

これらのトピックを通じて、依存型を利用した開発や定理証明がどのようなものであるのかを皆さんに知っていただけたら幸いです。そして、興味をもったらぜひ挑戦してみてください。みんなも定理証明、しよう！

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

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

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

• 入門

セッションの概要

関数型プログラミングに始めて触れる方にスキルを身につける/教えるためのトレーニング方法について紹介します。

私の所属先では、サーバサイドの言語として以前はPHPをメインとして開発していましたが、数年前から新規のシステムや既存システムのリプレイス時の言語としてKotlinを採用しています。
Kotlinは純粋関数型言語ではないですが関数型の特徴を持った言語であり、その恩恵を受けた開発が魅力のマルチパラダイムなプログラミング言語です。他方、PHPは比較的命令型・オブジェクト指向型の言語といえます。ゆえに、PHPを書いていた人がいきなり "Kotlinらしい" 関数型の言語機能を利用したコードを書けるようになるためには少々のハードルがあります。
そこで、Kotlinを用いた開発のオンボーディングとして初学者向けの問題集をトレーニング資料として用意し、自学自習を促すことでハードルを超えやすくする取り組みを始めています。

このセッションでは、その自学自習用の資料で具体的にどのような意図でどのような内容に触れているかを解説しつつ、効率的な学び方やペアプロを用いた教え方やついて触れられればと考えております。また、関数型言語の初学者にとって、どのようなことが関数型言語を学ぶ入口であるかのイメージが湧くようなセッションを目指します。

以下の内容をお話する予定です。

• どのようなことを学ぶ/教える必要があると考えているか
• 効率的に学ぶためにどのようなことをすればよいか
• テキストとしてどのようなものをよういしているか
• ペアプロや等を活用したハンズオンでの教え方について

よろしくお願いいたします。

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

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

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

• 理論
• 入門

セッションの概要

本セッションは、数理論理学を学ぶことによって型システム理論への入門が容易になると主張するものです。
発表者はかつて『型システム入門』の勉強会に参加していましたが、参加者の一部はプログラマではないにもかかわらず、ときに職業プログラマーである発表者よりも、深く内容を理解できていました。彼らは、数理論理学に深く通じているという点で共通していました。
なぜ数理論理学の知識が型システム理論の理解を助けるのでしょうか？それは、静的型付け言語における操作的意味論と型システムの関係が、論理学における意味論と証明体系の関係に対応するからだと発表者は考えています。つまり、論理学に詳しい彼らにとって、『型システム入門』の内容はとても馴染みのあるものだったのです。
そこで本発表では、『型システム入門』への入門を目論んでいる方々に向けて、あえて数理論理学を経由することを提案します。セッションは次のような内容を含みます。

• 論理学における意味論・証明体系の概要と、両者の関係
• 静的型付け言語における操作的意味論と型システムの概要と、両者の関係
• まとめとして、論理学と型システム理論の類似性

対象とする聴衆のレベル

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

セッションのテーマ

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

セッションの概要

並列分散処理は高いスケーラビリティを求められる一方で、タスク分割・通信制御・データ整合性など管理するべきことが多く、とにかく開発が複雑になりがちな領域です。
そういった課題に対し、アクターモデルはソフトウェアを「アクター」という小さなメッセージ駆動単位に分割することで、スケーラブルかつ扱いやすい計算モデルを提供します。
さらにアクター間のメッセージに静的な型を付けることで、不正な通信をコンパイル時に防ぐことができます。

トヨタ自動車では、Scalaの型付きアクターモデルライブラリPekkoを基盤として、人流シミュレータ・交通シミュレータ・ドライビングシミュレータ・VRなどをリアルタイムに連携する分散メッセージングフレームワークArkTwinをOSSとして開発しています。
ArkTwinでは大量の時空情報を低遅延で処理する必要があり、型付きアクターモデルの恩恵なしには実現できませんでした。

本セッションでは、ArkTwinの開発を通じて得られた知見をもとに型付きアクターモデルの利点と実装パターンについて紹介し、それらがもたらす分散シミュレーションの未来像についてお話します。

対象とする聴衆のレベル

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

なるべくSwift言語や関数型プログラミングの前提知識を必要としないように説明したいとは思いますが、たとえばクロージャが何かという説明などは省略します。

セッションのテーマ

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

セッションの概要

みなさんは関数型プログラミングの説明を読む時、「それで結局何ができるようになるのか？」または「どんな課題を解決するのか？」と感じたことはありませんか？私自身そう感じることが何度もあります。

本発表では、まずiOSアプリ開発を知らない方向けに、iOS開発で課題となる状態管理やコードのテストについて説明します。そして、それらが関数型プログラミングの考え方をベースにしたOSSフレームワーク『The Composable Architecture (TCA)』によって、どのようにシンプルな形で解決されるのかを解説します。

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

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

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

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

セッションの概要

昨年v1に達したGleamという静的型付けな関数型言語があります。
この言語はErlang VM(BEAM)とJavaScript(Node.js/Deno/Bun)で実行でき、ifやforなどが存在しないなど非常にシンプルな構文を持っているという特徴があります。

Erlang VMは並列性と耐障害性に優れた処理系で、
主にゲームサービスや通信システムなど大量に同時接続されたりサーバーや高い可用性が求められるシステムにおいて採用されています。

現在のGleamエコシステムはバックエンドフレームワークであるwispや、
フロントエンドフレームワークであるLustreなど様々なライブラリ・フレームワークが登場しています。

本登壇を通して始め方や周辺ツールの導入方法からGleamという言語の強みやエコシステムの現状、今後のGleamの可能性などを紹介していきます。

対象とする聴衆のレベル

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

セッションのテーマ

• Tips

セッションの概要

Scala歴10年超のエンジニアが、TypeScriptやPythonを書く際にScalaならこう書けるのに!というあるあるを紹介していきます。
型周りの話から、パフォーマンスの話まで、実際に業務で書いていて感じたところを紹介していきます。
TypeScriptやPythonで、関数型スタイルのライブラリを導入して無理やり実現してみて、それでもまだ足りない！ところまで踏み込みます。
Scalaに未練タラタラの内容です。

次のライブラリ/機能にも少し触れます

• FPTS
• Effect
• pandas
• Python TypeHinting

対象聴衆

• Scalaを使っていて、TypeScriptやPythonも同時に使っている人

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

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

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

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

セッションの概要

OBJファイルフォーマットから3Dジオメトリを読み込むために、elm-obj-fileパッケージを使ってデコーダーパターンを使う方法を説明します。OBJフォーマットにはglTFのシーングラフのような最新の機能はありませんが、デコーダーパターンを使うと：

• 3Dモデルの必要な部分だけを読み込めます（オブジェクト名、マテリアル、グループで）
• 複数のプリミティブタイプを読み込めます（点、線、三角形、面、テクスチャ付きメッシュ）
• 座標系と単位を変換できます
• シンプルなデコーダーを組み合わせて、複雑な形状を作れます

Blenderから作ったモデルをウェブアプリケーションに読み込む実例を示します。

トークの内容：

1. デコーダーパターンの説明
2. OBJフォーマットへのパターンの適用
3. Blenderとelm-3d-sceneやelm-physicsを使った実例

得られること：

• 複雑なデータフォーマットを解析するためのデコーダーパターンの使い方
• 関数型プログラミングによるファイルフォーマットの柔軟な扱い方
• Elmで3Dモデリングソフトとウェブアプリケーションを連携させる方法

対象とする聴衆のレベル

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

セッションのテーマ

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

セッションの概要

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

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

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

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

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

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

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

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

セッションの概要

ClojureScript をベースとした軽量なコンパイラである Squint を用いて React による Web フロントエンド構築のノウハウを発表します。関数型言語で Web フロントエンドを構築してみたい方におすすめの発表です。

Squint は ClojureScript のビルドツールの新星です。ClojureScript の開発環境は時代とともに変化してきました。
もともと ClojureScript は Clojure (Java) 由来のビルドツールを使ってきましたが、 徐々に npm との親和性を求められるようになり、それを高めたツールが登場してきました。
その中でも Squint は npm ライブラリとして使用することができ、 package.json だけで ClojureScript ライクな言語を vite などと組み合わせて気楽にビルドすることができるツールです。

Squint を使うと TypeScript を導入するのと同じくらいの気楽さで ClojureScript を導入でき、 JavaScript 向けのライブラリをそのまま使うことができるので、 ClojureScript の文化を知らなくても開発を始められます。
従来の開発ではどうしても ClojureScript の独自文化を開発者が理解している必要がありましたが、 Squint ではそのハードルは大きく下がります。

今までの JavaScript の資産を気楽に使いつつ、関数型言語のパワフルさを活用する新しい Web フロントエンド開発手法を皆様にお伝えします。

対象とする聴衆のレベル

• 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 実装、そしてサービス化された機能をそれぞれ参照しつつ解説します。