ABSTRACT. ビザンチン将軍問題は，故障プロセスに影響されることなくすべての正常プロセスが正しい値で合意する問題である．通常，ビザンチン将軍問題では故障の特定までは要求されないが，合意を達成すると同時に故障を特定する仕組みがあればシステムの信頼性向上に有益である．そこで本研究では，Lamportの提案したビザンチン将軍問題に対するアルゴリズムOMを拡張し，可能な範囲で故障を特定する仕組みを追加する．これを実現するための基本的なアイデアは，故障プロセスが誤ったメッセージを送信した際に生じる不整合を手がかりに，故障プロセスの候補を限定するというものである．このアイデアを定式化するために，数理論理学の一分野である認識論理に基づいて対象となるシステムをモデル化する．これにより，メッセージのやりとりの中で各プロセスがどのような知識を得るのかについて，認識論理の論理式およびそれらの性質を用いた議論が可能になる．

ABSTRACT. 原論文の出典： 　　Title: Intuitionistic Fixed Point Logic 　　Author: Ulrich Berger, Hideki Tsuiki 　　Journal: Annals of Pure and Applied Logic, Volume 172, Issue 3, March 2021, 102903 　　掲載予定

IFP (Intuitionistic Fixed Point Logic) は，直観主義一階述語論理に， strictly positive な，帰納的，余帰納的述語定義を加えた体系です。IFP の 実現可能性解釈により，公理的に定義された構造に関する数学的な証明から， 遅延評価的な関数型言語のプログラムを抽出することができます。その抽出は， 領域理論的な表示的意味論に従って行われ，抽出されたプログラムは Haskell 言語に翻訳することができます。その応用として，実数が，符号付き二進表現 を持てばグレイコード表現を持つということをIFP で表現し，その証明を行い， その証明からこれら２つの表現間の変換プログラムを抽出します。

(以下は補足説明です)

IFP の証明抽出は，Curry Howard 対応や BHK 解釈に基づいていますが， 証 明の対象となる構造は，Coq などの型理論ベースのシステムのように帰納的に データ型を定義ことによってではなく，一階述語論理を用いて公理的に定義し ます。そして，アルゴリズムが用いる再帰的な構造は，帰納的，余帰納的な述 語定義を通じて与えます。このように，対象をデータ表現と独立なものにする ことにより， 証明が通常の数学におけるものにより近くなり， 実数などの，一つの対 象上で，さまざまな帰納的構造に基づいたアルゴリズムを抽出することが可能 になります。原著論文は広範な内容を扱っていますが， 今回の発表は，このこと に重点をおいて行いたいと思っております。

IFP には，Prawf という実装が作られており，その中で IFP の証明を行い， プログラムを抽出し，実行することができます。Prawf システムについても， 昨年， Petrovska, O. が加わった３人の著者で， 国際会議 (CiE: Conference on Computability in Europe) にて発表を行いました。 発表では， これについても触れられればと思っています。

Berger, U, Petrovska, O, Tsuiki, H: Prawf: An Interactive Proof System for Program Extraction. In Proceedings of 16th Conference on Computability in Europe, CiE 2020, LNCS 12098: 137--158, 2020

ABSTRACT. Weakest precondition transformers are useful tools in program verification. One of their key properties is compositionality, that is, the weakest precondition predicate transformer (wppt for short) associated to program f;g should be equal to the composition of the wppts associated to f and g. In this paper, we study the categorical structure behind wppts from a fibrational point of view. We characterize the wppts that satisfy compositionality as the ones constructed from the Cartesian lifting of a monad. We moreover show that Cartesian liftings of monads along lax slice categories bijectively correspond to Eilenberg-Moore monotone algebras. We then instantiate our techniques by deriving wppts for commonplace effects such as the maybe monad, the non-empty powerset monad, the counter monad or the distribution monad. We also show how to combine them to derive the wppts appearing in the literature of verification of probabilistic programs.

This paper has been already published in MFPS '20 (https://www.monoidal.net/paris2020/mfps/)

ABSTRACT. Dependent refinement types are types equipped with predicates that specify preconditions and postconditions of underlying functional languages. We propose a general semantic construction of dependent refinement type systems from underlying type systems and predicate logic, that is, a construction of liftings of closed comprehension categories from given (underlying) closed comprehension categories and posetal fibrations for predicate logic. We give sufficient conditions to lift structures such as dependent products, dependent sums, computational effects, and recursion from the underlying type systems to dependent refinement type systems. We demonstrate the usage of our construction by giving semantics to a dependent refinement type system and proving soundness. This paper is accepted to FoSSaCS 2021.

ABSTRACT. Rubyは静的な型付けを行わない「動的型付け」のプログラミング言語として開発されました．この特徴はメタプログラミングの活用を推進し，Ruby on Railsなどの広く利用されるソフトウェアを実現する基礎となってきました．その一方で，プログラムの挙動を静的に検査あるいは理解することを困難とし，特に大規模な開発において不利益となる点が多かったことも事実です．2020年末に公開されたRuby 3では「静的な型検査の提供」が重要な機能追加の一つとなり，講演者を含む多くの開発者が労力を注いできました．この講演では，Ruby 3の型検査はどのようなものになるのかを紹介し，その背景にはどのような動機・要求・制約があり，どのような議論や妥協があったのか，特に実用的なプログラミング言語の機能開発という観点を重視して話をします．

ABSTRACT. Felleisen et al.'s control and prompt are a variant of delimited control operators that exhibit sophisticated behavior. The behavior comes from the ability to manipulate the invocation context of captured continuations, which enables implementing non-trivial algorithms but complicates the semantics of programs. We present our preliminary work on designing a general type system for control/prompt. Following previous studies on typing control operators, we identify necessary typing constraints by carefully analyzing the CPS translation. As a result, we obtain a terminating type system that allows modification of trail types.

This paper has been presented at PEPM 2021.

ABSTRACT. The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. Existing approaches to this problem are classified into two groups: one for restricting how effects are triggered and the other for restricting how they are implemented. This work explores a new approach to ensuring the safety of polymorphic effects in polymorphic type assignment. A novelty of our work lies in finding a restriction on effect interfaces. To formalize our idea, we employ algebraic effects and handlers, where an effect interface is given by a set of operations coupled with type signatures. We propose signature restriction, a new notion to restrict the type signatures of operations, and show that signature restriction is sufficient to ensure type safety of an effectful language equipped with unrestricted polymorphic type assignment. We also develop a type-and-effect system to enable the use of both operations that satisfy and do not satisfy the signature restriction in a single program.

出典: Proc. ACM Program. Lang. 4, ICFP, Article 117 (ICFP 2020) 掲載済み

ABSTRACT. 本研究では，定理証明支援系Mizarで書かれた数学ライブラリをホスティングするWebプラットフォームを開発した．すでに数学定理の解説をWiki形式で編集・閲覧する機能，シンボルとファイルを検索する機能，シンボル定義や定理引用などの参照先へのハイパーリンク機能が実装済みである．また，本プラットフォーム上で作成されるコンテンツは，ライブラリ更新時にもリンク関係が保たれるように設計されている．本プラットフォームは機能拡張を考慮して設計されており，今後も定理検索，ライブラリ依存関係のグラフ表示などの機能を追加する予定である．

ABSTRACT. 本研究ではモデル検査を用いた交通輸送システムの近似スケジューリング手法を提案する．特にここでは，隊列走行可能な交通システムを対象に，輸送量や車両の台数に関する制約のもとでの輸送時間や輸送量の最適化を目的とする．その基本的なアイデアは，運行経路のネットワークを複数のエリアに分割し，また単位時間の粒度を大きくする抽象化を行うというものである．これによりモデル検査でしばしば直面する状態爆発問題を回避し，スケジューリングの高速化と拡張性の向上を行った．

ABSTRACT. 非連結パターンマッチングは関係データベースを用いるSQLなどの宣言型言語やProduction Systemで応用されている一方, このマッチングが多いプログラムでは非効率な探索を行い実行時間が増えてしまうことがある. グラフ構造を簡明に書けるLMNtalも非連結サブグラフパターンマッチングの際に同様の問題が起きる. それはLMNtalの仮想機械SLIMが探索履歴を保持しない場合, 重複したマッチングをしてしまうためである. 本研究ではグラフの頂点を表すアトムにおいて履歴管理用アトムの導入およびアトムの整列によって高速化を図った. 本手法により時間計算量を減らし, 予測可能な時間計算量に改善することができた.

ABSTRACT. 我々は関数型言語Elixir向けのデータ並列スケルトンライブラリ Pelemay と PelemayFp を研究開発してきた。また，これらを人工衛星からの膨大な画像処理を高速化するために用いるべく，OpenCVと連携したExcvを試作してきた。これらの研究により，現在のElixirの実行基盤であるErlang VM(BEAM)では，用意されている2つのFFIであるNIFとPortのいずれも，Elixirから並列に呼び出す時に極めて大きなペナルティを受けることが明らかになった。本発表では，Pelemay, PelemayFpを実行する様子をデモンストレーションし，それぞれの原理を概説する。 なお，Elixir原作者であるJose Valimが，Project Nx (Numerical Elixir) を発表する。2021年2月10日時点でNxの詳細は明らかになっていないが，Pelemayシリーズに触発されてJose自らが開発した，プロダクションにも使えるOSSであるということである。研究用途のOSSであるPelemayシリーズを開発した我々としては，本望である。今後，Nxについても性能評価を詳細に行い，さらなる研究開発を進めたい。

ABSTRACT. 近年，自然言語間の翻訳は，NMTを用いることで飛躍的に精度が向上している．我々は，NMTをPythonと日本語間の翻訳に適用することによって，自然言語間のような高精度翻訳の実現を目指した．本発表では，Pythonの内容を示すのに適した表現を得るために行った記号に対する処理や，日本語文のサブワード分割などの前処理をはじめ，seq2seqとTransformerを用いたPythonと日本語間の翻訳結果について述べる．併せて算出したBLEUスコアは，Pythonから日本語への翻訳，日本語からPythonへの翻訳の双方において高いスコアを記録した．本発表では，実験の内容や結果を述べるとともに，今後の展望についても議論したい．

ABSTRACT. Tascell is a work-stealing based task-parallel programming language which supports intra- and inter-node dynamic load balancing. There have been proposed several MPI-based implementations for inter-node communication in Tascell. Among them, an implementation called Tascell/MT achieves the best performance for many applications. However, Tascell/MT has two problems: a worker always copies data into/from a buffer before sending/after receiving it to/from an external node, and when a worker receives large input data, a computing core assigned to the worker becomes idle until the data transfer is completed. We propose two Tascell implementations, called Tascell/DR and Tascell/LH, to solve these problems. In Tascell/DR, a worker sends/receives the task's input data directly without using a buffer. Tascell/LH allows a worker to start a task received from a remote node before the transfer of the task's input data is completed; part of the input data is transferred concurrently with the execution of the task. We evaluated the proposed implementations on the Laurel 2 supercomputer of Kyoto University. We confirmed that Tascell/DR can reduce the time for transferring input data of tasks. It also achieved better performance especially for backtrack search applications. Tascell/LH achieved the best performance for a benchmark in which arrays are frequently transferred among computing nodes as input data of tasks.

ABSTRACT. 人間が心地良いと感じる音楽を作るためには、さまざまな規則に従う必要がある。 これらの規則は、良い音楽が満たすべき仕様とみなすことができる。 定理証明の分野では、あるプログラムが仕様を満たすことを示すために、 依存型を用いて仕様を表現し、その型をもつ証明項を構成するという手法が取られている。 本研究では、この手法を音楽理論に応用する。 具体的には、対位法の規則を定理証明支援系 Agda で形式化する。 対位法とは、複数の旋律を重ね合わせるための理論であり、 和音の距離や進行に関する規則をもつ。 本発表では、これらの規則を依存型として自然に表現できることを示す。 また、実際に証明を付けた「良い音楽」と、規則を破った「悪い音楽」の例を提示する。

ABSTRACT. Parsing expression grammar (PEG)に基づくパーサは、バックトラックを行い文字列の無制限の先読みを許す再帰下降構文解析を行う。 PEGパーサでは、バックトラック先と規則呼び出しのリターン先の両方をスタックに保持することから、末尾呼び出しなどの解析表現を含む文法の解析効率が悪くなるという欠点をもつ。 本発表では、Prolog処理系であるWarren Abstract Machine (WAM)で用いられている最適化手法から着想を得て、仮想マシン方式のPEGパーサに対してスタック上のエントリを削減する手法を導入する。

ABSTRACT. プログラム検証において篩型は広く活用されている。しかし再帰的データ構造を扱うプログラムの全自動検証に対して、既存の篩型システムは不十分である。なぜなら、それらの篩型はデータの様々な特性を統一的に記述できず、一般の性質の表現にはユーザによる定義が必要なためである。そこで我々は新たな篩型システムを定義し、整数引数付き再帰篩型を導入する。この篩型は再帰的データ構造の多様な特性を表現する一般的な形式を与える。本手法では、まずプログラムの検証問題を篩型の型付け可能性問題に帰着し、次にそれを∀∃-CHCの充足可能性問題に帰着することで解く。この手法に基づいて検証器を試作し、実験により効果を確認した。

ABSTRACT. Homotopy type theory (HoTT) は依存型理論の一種であるMartin-Löf型理論の拡張であり、homotopy論についての推論を始めとして、定理証明支援系への応用が知られている。 HoTTの主なモデルとしてはsimplicial setのなす圏などが挙げられるが、本研究ではsimplicial setの“アーベル化”であるchain complexをモデルに持つような型理論を構築する。これによりホモロジーについての推論ができるようになるだけでなく、path type を糖衣構文として定義することのできるnull typeという新しい型構成子を発見した。

ABSTRACT. 形式検証を用いたテスト手法にブラックボックス検査がある。ブラックボックス検査は、入力としてブラックボックスなシステムと時相論理式で記述された仕様をとり、システムが仕様を満たすか否かを出力する。ブラックボックス検査を物理情報システムのテストに用いる際には、実行時間の長さが実用上の課題となる。これはブラックボックス検査ではシステムを数多く実行する必要があるが、物理情報システムのシミュレーションは長い時間を要するためである。本研究では、テスト対象の仕様を構文的に書き換えて意味を強め、強めた仕様も用いてブラックボックス検査を行うことで、システムのシミュレーションの回数を減らす最適化手法を提案する。

ABSTRACT. 本研究では，タスク並列言語の性能評価に利用されるUTS（Unbalanced Tree Search）ベンチマークを用いて階層的計算省略に基づく並列実行モデルHOPEの性能評価を行った．HOPEモデルは並列計算環境向けに良好な負荷分散と耐障害性を備えている．UTSは，様々な形状のばらつきのある木を動的に生成し，探索を行うことでノード数を数え，その探索完了までの時間を計測することで評価を行う．性能評価の結果，HOPEは末広がりで高さが限定的な探索木では高い並列効率を示したが，同世代ノード数が期待値としては次第に減っていく高さ（世代数）が大きな探索木では並列効率は低下した．性能改善には自然な分割統治だけでない探索上の工夫が必要だと考えられる．

ABSTRACT. 既存のparsing expression grammar (PEG)に基づくパーサは、ナイーブな実装では解析が指数時間を要する恐れがあり、メモ化により線形時間に抑えても入力長に比例したメモリを要する欠点がある。また、バックトラックと構文エラーの区別がつけられない為、エラー処理が困難であるという欠点がある。 本発表では、PEGのバックトラックを抑制する方言であるCommitted-Choice PEGに基づき、ATNの表引きで解析するパーサの生成系と、入力文字の挿入・削除によるエラー処理をそれぞれ実装し、それぞれの欠点の解決を試みる。

ABSTRACT. MetaOCamlはOCamlの多段階プログラミング拡張であり，メタプログラムがwell-typedならば生成されるプログラムもwell-typedであることが保証される．本研究ではCプログラムで制御される自律型ロボットに対して，MetaOCamlでCコードを生成することにより，Cで直にコードを書くよりも高い安全性と記述性を実現する方式を考える．ここでいう安全性とは実行時型エラーが起こらないこと，記述性とは簡潔な記述が可能であることを指す．具体的には，MetaOCamlのoffshore機能を用いて教育用ロボットC-cubicのCプログラムを生成するOCamlライブラリを実装し，いくつかの例題で記述・動作テストを行う．

ABSTRACT. Most modern programming languages, such as Java, JavaScript, and PHP, have a just-in-time (JIT) compiler for achieving their fast runtime. Method-based compilation and trace-based compilation are two major compilation strategies, and they have their advantages and disadvantages. To incorporate the benefits of both, we proposed a meta-hybrid JIT compiler framework and its proof-of-concept implementation called BacCaml. It can generate a virtual machine with a JIT compiler that can use the two strategies from an interpreter definition. As a next step, we move on to a more practical framework to show that the meta-hybrid JIT compilation is useful for many languages. This presentation presents a sprouting idea for supporting the two strategies in a meta-tracing JIT compiler. This approach does not extend the compiler itself but designs an interpreter to enable the two compilation strategies in RPython.

ABSTRACT. 本研究ではOCamlプログラムの計算過程を1ステップごとに出力するプログラムであるOCamlステッパを用いる。先行研究ではOCamlバージョン4.04.0用に作られていたが、本研究ではOCamlの最新バージョンである4.11.1に対応させ、コンテキストを変更、その後try文とmoduleを実装した。moduleについては同ファイル内のモジュール宣言一般を対象に実装する。この時、モジュールが含まれるプログラムをどう実行すれば良いかを検討し、明らかではなかったステップ実行を見出した。今後はモジュール宣言の表示改善や別ファイルのモジュール宣言などを実装しより良いステッパを目指したい。

ABSTRACT. In the last few years, GPUs became ubiquitous: from high-performing server machines to low-power mobile devices. Such diversity made it increasingly difficult to achieve high performance across different architectures. Lift tries to solve this problem generating many programs by exploring an optimization space made of many rewrite rules. However, naturally, it lacks many modern architecture-specific optimizations present in expert hand-crafted programs. The SSAM model, for example, is a recent developed scheme based on systolic arrays for increasing reuse on memory-bounded problems, making use of fast shuffle instructions present on GPUs. They demonstrate the potential of their approach with stencil applications, such as convolutions and iterative stencils. We argue that the Lift framework can accomodate such an optimization, since SSAM itself is general. Yet, its original paper described it informally, which hindered its general use. As such, we propose a new, stricter, formalization for the SSAM model. This formalization allows us to extend Lift with a new rewrite rule and primitives, without loosing generality. We believe that our effort narrows the gap between hand-crafted architecture-specific programs and portable Lift programs.

ABSTRACT. 定理証明支援器上でアルゴリズムの計算量をフォーマルに証明する研究はいくつか存在する（[Guéneau, Charguéraud, Pottier 2018][Zhan, Haslbeck 2018]他）。その中でも既存研究[McCarthy et al. 2018]では、抽象的な計算ステップ数をカウントするモナドを用いて，バランス二分木のinsert操作などの計算量の証明を行なっていた。 　本研究ではこの既存研究を二つの点で改良する。まず、既存研究の証明中に登場する、例えば6 + 9 log nの6や9などの具体的すぎる定数値を、k1 + k2 log nのように一般化する。また、既存研究では間接的にしか証明されていなかった計算量の漸近的オーダーも、プログラムの型自体に含めて証明する。その過程で、既存研究の計算量モナドのCoq上の定義は十分に抽象化されておらず、使い方に注意しないと無意味な「証明」が書けてしまうことがわかった。

ABSTRACT. 代数的エフェクトとは，例外や状態などの計算エフェクトを表すための機構である．代数的エフェクトを特徴に持つプログラミング言語としてKoka言語がある．Koka言語のコンパイラでは高階の多相型と代数的エフェクト，エフェクト強制を特徴に持つ明示的型付けの中間言語が用いられている．この中間言語の形式化である System Fe には，エフェクト強制が含まれていなかった．本研究では，System Fe にエフェクト強制を導入した計算体系 System Fe+openを定義し，健全性を証明する．System Fe+open では，System Fe の健全性を示す上で必要な補題が成り立たないため，証明全体を一から再構成する．

ABSTRACT. 本研究では、レコードとハッシュテーブルの暗黙な相互運用が可能なプログラミング言語の実現を目標とする。この暗黙な相互運用によって、開発の初期段階では、動的な構造を持つハッシュテーブルを用いた柔軟なプロトタイピングを許しつつ、開発が進み実装方針が固まり次第、ハッシュテーブルを静的な構造を持つレコードに漸進的に置き換え、頑健で効率の良いプログラムへの移行が可能になる。本研究では、Ohoriの多相レコード計算を、ハッシュテーブルが受け入れられるように拡張し、型推論、及び実行時のデータ変換を伴なわないようなコードを生成するコンパイルアルゴリズムを提案した。

ABSTRACT. 単一化は、変数を含むある二つの項を同一にできるような解代入を見つける操作で、自動証明に使われる重要な操作の一つである。 本研究は、単一化のうち、項にラムダ計算を含む高階パターン単一化を対象とする。 単一化の解を導出するシステムを、Weirich らが開発した Haskell ライブラリ Unbound を用いて実装した。 アルゴリズムは Miller が開発した高階パターン単一化を Nipkow が関数型言語で表したものを基礎とした。 システムに Unbound を用いるときのモナド的プログラミング手法や、用いることによって得られるメリットをまとめ、同様のシステムを開発するときの参考になることを目的としている。

ABSTRACT. 入出力をランク付き木とする累積引数付き再帰関数のモデルであるマクロ木変換器（MTT）は，表現可能な関数のクラスが合成に関して閉じていない．だが，ある条件下では複数のMTTの融合が可能であることがいくつかの先行研究から知られている．本研究では，任意個のMTTの融合を目的とした阿部の手法に注目した．この融合手法では複数のMTTを等価な1つの高階木変換器（HTT）に変換し，得られたHTTがある条件を満たす場合に限り，その階数を下げることでMTTの融合を達成する．本研究では，同論文で未達成であるHTTからMTTへの変換手法の定式化および既存研究との比較を目指す．

ABSTRACT. デザインレシピは、関数を定義する際に考えるべきことや書くべきことを6つのステップにまとめたものである。デザインレシピを使うことで、プログラミング初学者は各ステップで何をすべきかが明確になる。しかし、途中のステップの結果は、実行可能なコードでないこともあり、それらが適切かどうかは判断できないこともしばしばある。 本研究の目標は、デザインレシピに基づいたプログラミングに特化したプログラミング環境を作ることである。 そのために、デザインレシピの各ステップでフィードバックを生成するためのDSLを実装する。

ABSTRACT. We report on an on-going formalization of measure theory in the Coq proof assistant. This effort is part of the MathComp-Analysis library, which aims at a formalization of analysis that takes advantage of the Mathematical Components library for algebra. We explain the development of basic infrastructure such as support for extended reals, infinite sums, and mathematical structures for measures, as well as the road to the formalization of Lebesgue measure.