PPL2022では，以下の2件の招待講演を予定しております．
| 古瀬 淳 | ダイラムダ株式会社 |
|---|---|
| ブロックチェーンと形式検証 ～ Tezos の場合 | |
| 諏訪 敬之 | SATySFi開発者 |
| 静的型つき函数型組版処理システムSATySFiの紹介 |
古瀬 淳（ダイラムダ株式会社）
中央管理者のいない分散データベースであるブロックチェーンでは、各サーバノードの運営コストやデータ改竄を防ぐためのインセンティブとして、換金性のあるトークンの導入がどうしても必要になります。結果、ブロックチェーンには巨額の金銭的価値が保持されます。この「お金」との切っても切れない関係、そしてソースコードが全公開されるという性質により、ブロックチェーンシステムに深刻なバグがあった場合、それを突いた巨額のトークン窃盗が起きかねません。このように高い安全性が求められるブロックチェーンでは形式検証は非常に強力な安全化手段となります。 Tezosブロックチェーンでは、安全なシステムの構築を目指しその大きな実装単位である経済プロトコル、プロトコルを使ってブロックの検証を行うシェル、そして契約の自動執行を行うアプリケーションであるスマートコントラクト、それぞれの重要部品に対し実際に形式検証を行っています。本講演ではこれらの検証例のいくつかを紹介します。
諏訪 敬之（SATySFi開発者）
SATySFi（サティスファイ）は講演者が2017年度のIPA未踏事業の1プロジェクトとして支援のもと開発し，現在も発展を続けている比較的新しい組版処理システムである．SATySFiでは静的型つきのいわゆる函数型言語によってパッケージ或いは文書そのものの一部を書くことができ，一般的なプログラミング言語に近い意味論による高いカスタマイズ性や，型システムによる或る程度原因のわかりやすいエラー報告を実現していることを特徴としている． 本講演では，PPLに参加される方々の興味を鑑みて，特に組版処理や文書作成といった用途に要請されてSATySFiに導入した，意味論や型システム上特徴的な機能について紹介する．講演時点での開発の進展状況によっても紹介できる内容は多少変化しうるものの，主として組版処理特有の組み込み函数がどんな型をもつ定式化になっているかや，（多段階計算やモジュールシステムなどの）より広汎な目的で研究されてきた型システムの理論がどのようにSATySFiで活用されているかについて，デモ等を交えつつ概説したい．