ABSTRACT. 項書き換えシステム(TRS)による計算解の一意性を保証する性質として合流性がある．条件付き項書き換えシステム(CTRS)はTRSの書き換え規則に条件を付加して得られる計算モデルであり，関数型プログラムを考える場合にはより自然なモデルである．CTRSの計算の階層ごとに合流性が成立する性質を階層合流性という．階層合流性の十分条件はあまり多くは知られていないが，そのうちの一つは，CTRSが真指向式かつ右安定な直交3-CTRSになっていることである(鈴木ら,1995)．一方，TRSの場合，直交TRSの合流性の拡張として，左線形TRSの合流性を保証する様々な危険対条件が得られている．本論文では，直交3-CTRSに対する階層合流性の証明と，並列に閉じた左線形TRSに対する合流性(外山,1987)の証明を組み合わせることによって，指向式の左線形3-CTRSに対する階層合流性を保証する危険対条件を与える．

ABSTRACT. 項書き換えシステムにおいて，全ての基底項が構成子項に簡約できるという性質を十分完全性という．これは，直感的には関数プログラムが全ての入力に対して計算解をもつかという性質に対応する．十分完全性は項書き換えシステムにおける帰納的定理の自動証明に重要な役割を果たしている．項書き換えシステムが停止性を持つ場合の十分完全性については判定法が知られている．一方，停止性を持たない場合については，あまり研究が進んでいない．そのような項書き換えシステムについては，計算解を持つべき対象として全ての基底項を考えるのではなく，特定の形の基底項を対象とした局所十分完全性を考えることが適当である．実際，帰納的定理の証明法として，局所十分完全性を利用した潜在帰納法(菊池&篠埜，2018)が提案されている．本論文では，停止性を持たないような項書き換えシステムにも適用可能な局所十分完全性の証明手法を提案する．

ABSTRACT. Geuversらによって提案された 汎用的自然演繹 (Truth-table Natural Deduction) とは， 任意の結合子についてその真理値表から機械的に推論規則を構築することができる枠組み であり，一般的でない結合子に対しても推論規則を構築することができるという利点がある． Geuversらは，直観主義論理および古典論理に対応する汎用的自然演繹の体系 IPCとCPCと、IPCに対する証明正規化を定義し、部分論理式性と強正規化性を 示すことにより，IPCの基本的性質である無矛盾性や決定可能性を証明している． しかし，CPCに対する証明正規化については未だ議論されていない．実際，CPCに対して 部分論理式性などの良い性質をもつ証明正規化の概念を定義することは困難であると考えられる． そこで本論文では，古典論理に対する新たな汎用的自然演繹としてIPCμとその証明正規化を提案する．IPCμはIPCの拡張であり，Parigotの古典自然演繹の要領で結論に複数の論理式を 認めるようにしたものである．このため，Parigotの古典自然演繹にCurry-Howard対応する lambda-mu計算のアイディアを用いればIPCμの証明正規化が容易に定義することができる． 本論文では，IPCμが証明可能性の意味でCPCと同等であることを示し，その証明正規化に ついて部分論理式性と強正規化性を示す．これらの結果より，IPCμの無矛盾性や保守性などの 基本的な性質が得られる．IPCμの強正規化性は，van der GiessenによるIPCの強正規化性 と同様にCPS変換を用いて証明されるが，既存の証明の単純な拡張では証明できない．本論文では， IkedaらによるCGPS変換を用いてIPCμの強正規化性を証明する．

ABSTRACT. The engineering properties of programs derive from their design. As programs grow in scale and complexity, ensuring compliance with the overall design intent becomes more critical yet also more difficult. The goal of the Wyvern programming language is to help programmers cleanly express and enforce design as an integral part of programming. Wyvern accomplishes this with a capability-safe object model that expresses design constraints constructively, a strong system of types and effects to enforce abstractions at both component and object scales, and an extensible syntax that can express designs in a variety of domains while preserving important security and modularity properties. The talk will flesh out these design goals and demonstrate how the features of the language support them, while highlighting some research directions that have arisen from the language's goals.

ABSTRACT. Throughout the history of functional programming, recursion has emerged as a natural method for describing loops in programs. However, there does often exist a substantial cognitive distance between the recursive definition and the simplest explanation of an algorithm even for the basic list processing functions such as map, concat, or unique; when we explain these functions, we seldom use recursion explicitly as we do in functional programming. For example, map is often explained as follows: the map function takes a function and a list and returns a list of the results of applying the function to all the elements of the list. This paper advocates a new programming paradigm called pattern-match-oriented programming for filling this gap. An essential ingredient of our method is utilizing pattern matching for non-free data types. Pattern matching for non-free data types features non-linear pattern matching with backtracking and extensibility of pattern-matching algorithms. Several non-standard pattern constructs, such as not-patterns, loop patterns, and sequential patterns, are derived from this pattern-matching facility. Based on that result, this paper introduces many programming techniques that replace explicit recursions with an intuitive pattern by confining recursions inside patterns. We classify these techniques as pattern-match-oriented programming design patterns. These programming techniques allow us to redefine not only the most basic functions for list processing such as map, concat, or unique more elegantly than the traditional functional programming style, but also more practical mathematical algorithms and software such as a SAT solver, computer algebra system, and database query language that we had not been able to implement concisely.

ABSTRACT. 本研究では，入出力例となるテーブルをもとにSQLクエリを合成する手法を提案する．本手法は，スケッチの生成とその具体化という既存研究のアプローチにもとづくが，出力例の情報を合成が成功するための必要条件として表現しスケッチに伝播させることで，ボトムアップなスケッチの具体化を効率的に実現する．これにより，本手法は(1)サブクエリ等を含む複雑なクエリの合成を実現し，(2)入出力例として従来手法より規模の大きな，実データに近いテーブルを利用可能とした．手法の評価として，先行研究のベンチマークに加え，自社の実際のシステムに存在する SQL クエリをもとに作成した独自のベンチマークに対して合成を実行し，提案手法の有効性を示した．

ABSTRACT. This paper proposes a fluent API generator for Scala, Haskell, and C++. It receives a grammar definition and generates a code skeleton of the library in the host programming language. The generated library is accessed through a chain of method calls; this style of API is called a fluent API. The library uses the host-language type checker to detect an invalid chain of method calls. Each method call is regarded as a lexical token in the embedded domain specific language implemented by that library. A sequence of the lexical tokens is checked and, if the sequence is not acceptable by the grammar, a type error is reported during compilation time. A contribution of this paper is to present an algorithm for generating the code-skeleton for a fluent API that reports a type error when a chain of method calls to the library does not match the given LR grammar. Our algorithm works in Scala, Haskell, and C++. To encode LR parsing, it uses the method/function overloading available in those languages. It does not need an advanced type system, or exponential compilation time or memory consumption. This paper also presents our implementation of the proposed generator. This paper was presented in OOPSLA 2019.

ABSTRACT. Context: The algorithms for generating a safe fluent API are actively studied these years. A safe fluent API is the fluent API that reports incorrect chaining of the API methods as a type error to the API users. Although such a safe property improves the productivity of its users, the construction of a safe fluent API is too complicated for the developers. The generation algorithms are studied to reduce the development cost of a safe fluent API. The study on the generation would benefit a number of programmers since a fluent API is a popular design in the real world.

Inquiry: The generation of a generic fluent API has been left untackled. A generic fluent API refers to the fluent API that provides generic methods (methods that contain type parameters in their definitions). The Stream API in Java is an example of such a generic API. The recent research on the safe fluent API generation rather focuses on the grammar class that the algorithm can deal with for syntax checking. The key idea of the previous study is to use nested generics to represent a stack structure for the parser built on top of the type system. In that idea, the role of a type parameter was limited to internally representing a stack element of that parser on the type system. The library developers could not use type parameters to include a generic method in their API so that the semantic constraints for their API would be statically checked, for example, the type constraint on the items passed through a stream.

Approach: We propose an algorithm to generate a generic fluent API. Our translation algorithm is modeled as the construction of deterministic finite automaton (DFA) with type parameter information. Each state of the DFA holds information about which type parameters are already bound in that state. This information is used to identify whether a method invocation in a chain newly binds a type to a type parameter, or refers to a previously bound type. The identification is required since a type parameter in a chain is bound at a particular method invocation, and that bound type is referred to in the following method invocations. Our algorithm constructs the DFA by analyzing the binding time of type parameters and their propagation among the states in a DFA that is naively constructed from the given grammar.

Knowledge and Importance: Our algorithm helps library developers to develop a generic fluent API. The ability to generate a generic fluent API is essential to bring the safe fluent API generation to the real world since the use of type parameters is a common technique in the library API design. By our algorithm, the generation of a safe fluent API will be ready for practical use.

Grounding: We implemented a generator named Protocool to demonstrate our algorithm. We also generated several libraries using Protocool to show the ability and the limitations of our algorithm.

---

<Programming> 2020 発表予定

ABSTRACT. As a dependently-typed functional programming language, Idris shows quite a high expressiveness with its type system, without losing the safety of static checking.

To integrate the advantages brought by Idris into existing applications of other programming languages, we need to implement code generation back ends to run our safe and expressive Idris programs in the target language. While Idris is provided with a pretty convenient interface for code generation, as an interface in this topic is still cumbersome to implement and there're so many programming languages widely-used over the world, which will certainly bring about notable restrictions to the use of Idris.

To address this, we introduce a "common" intermediate representation, which helps to reuse the most part of an implementation of Idris code generation interface for distinct implementations. By this approach, making a back end for Idris becomes a small task and one can implement an Idris code generation back end in few hours or minutes.

ABSTRACT. OCaml Blocklyとは、ブロックなどのオブジェクトを組みたててプログラミングができる、型システムや変数束縛を直感的なユーザインタフェースとして備えた、OCamlビジュアルプログラミングエディタのことである。本研究では、遊ぶことで関数的な感覚が身につく、OCaml Blocklyを使用したゲームを考案、そして作成した。このゲームは、実行すると時間の経過に伴って、青空の下飛行機が飛行機雲を残しながら関数の軌跡を描く形となっている。これによって関数を飛行機の移動という形で直感的に理解できるようにする。段階を追ってゲームクリアしていくことで、xの一次関数や二次関数について学ぶことができる。

ABSTRACT. PEGの開発支援を行うために，本研究室で開発したPackrat parserライブラリWoodratに対して，アルゴリズミックデバッガを提案する．このデバッガは，プログラムの再帰的な実行のトレースを木構造で表現し，その木構造に対してデバッグを行うことを可能とする．そして，ユーザからの入力を元にバグが存在すると考えられる範囲を狭めて，木構造のエラー個所を半自動的に特定する．アルゴリズミックデバッギングで用いられているいくつかのアルゴリズムを導入し，PEGに即したデバッガを実装した．また，このデバッガを用いて，バグの発見が困難であるいくつかの文法に対して役立った例を示す．

ABSTRACT. 　項書き換えシステム(TRS)は，等式論理に基づく計算モデルであり，その性質の一つに簡約に関する一意正規形性(UNR)がある．また，各ルールの深さが高々1であるTRSをフラットTRSとよび，本発表ではフラットTRSに対するUNRが決定不能であることを報告する． 　UNRよりも強い性質に合流性(CR)と可換性に関する一意正規形性(UNC)があり，フラットTRSに対しては，CRが決定不能(大山口ら，2006)，UNCが決定可能(Radcliffeら，2017)ということがすでに知られている．本発表は，大山口らの証明の際に用いられたTRSにいくつかのルールを付け加えることによって，フラットTRSに対するUNRが決定不能であることを報告する．

ABSTRACT. 無線センサーアクターネットワーク(WSAN)は物理環境に配備された複数個の計算機が相互に通信することで、物理環境の観測や環境への働きかけを行う分散システムである。その実現にはセンサーノードに加え、環境への働きかけなどを行うアクターノードを含む複雑なノード間協調が必要である。アクターノードを含まない無線センサーネットワーク(WSN)については、マクロプログラミングと呼ばれる、WSN全体を一つの計算システムとみなしてその動作を記述する手法がある。本研究ではWSAN向けのマクロプログラミングのための言語を提案する。

ABSTRACT. 関数型言語 OCaml のブロックプログラミング環境である OCaml Blockly の改良をして新たな機能を付け足したのでそれを報告する。先行研究の時点では初学者向けに授業を行えるくらいまでの段階にはあったが、マウス操作しかできず、undo機能も使えない状態だった。そこで、より使いやすくしてOCaml Blockly を使い続けてもらうためにUndo機能の実装と、マウス操作のみでなくキーボード操作も可能になるようにOCaml Blockly を改良した。それぞれの機能の問題点を洗い出し、改良した結果どのように新たな機能を使えるようになったかを説明する。

ABSTRACT. Trace-based and method-based compilation are two major compilation strategies in JIT compilers. In general, the former performs well in compiling programs with deeper method calls and more dynamic branches, while the latter is suitable for any kind of program.

There is no clear winner between those two strategies; instead, each of them works better for different kinds of programs. It is straightforward to combine those two strategies; i.e., when compiling a different part of a program, using a strategy that works better for that part.

In this work, we propose a fundamental mechanism for compiling with both trace- and method-based strategies. Instead of developing a compiler for one particular language, we provide such a mechanism in a meta-compilation framework, which produces a virtual machine with a JIT compiler from an interpreter definition of a programming language.

We extend a meta-tracing JIT compiler, as a design choice and support trace- and method-based compilations on it. Therefore, we realize the method-based compilation by extending the compiler framework. Besides, we propose a mechanism to integrate two kinds of JIT compilation strategies, namely Stack Hybridization. Stack hybridization enables the runtime to go back and forth between the native code generated from different strategies as a single execution.

As a proof-of-concept, we implement a simple meta-tracing JIT compiler framework in the MinCaml compiler by following RPython’s architecture and extend it to support both trace- and method-based compilations and the stack hybridization mechanism. We evaluate the performance of our hybrid compilation approach by creating a small functional programming language with BacCaml and comparing it with MinCaml.

ABSTRACT. 微分λ計算は微分演算子を備えたλ計算の拡張であり、プログラムの非決定性や線形含意、Taylor展開などの豊かな概念を含む。また、Taylor 展開によって任意のプログラムを線形プログラムの和として表せることが知られている。

先行研究ではuntyped及びsimply typedな微分λ計算が主に扱われていたが、本研究ではこれをproduct type, dependent typeを用いてさらに拡張し、その圏論的モデルについて調べる。

ABSTRACT. メモリリークやNULL参照などのメモリエラーは、ヒープを操作するプログラムにおいて重大な欠陥となる。ヒープを必要とするデータ構造は再帰的なものが多く、それを扱うプログラムもしばしば再帰的である。そこで、メモリ状態をうまく記述できる分離論理を用いて、再帰プログラムにメモリエラーがないことを自動で検証するツールを実装した。

ABSTRACT. 構造化されたデータを扱う変換の解析や最適化のため，様々な計算モデルが考えられてきた．そのひとつとして木変換器があり，その理論は非常に有用である．しかし，古典的な木変換器理論は，構文解析器をはじめ扱うことのできない変換も多い．このため，構文解析器を含むより広い範囲の変換を扱うことのできる，スタック機構を搭載した木変換器のクラス，スタック木変換器が中野により提案された．しかし，スタック木変換器はまだ明らかにされていない部分が多く，応用を考える上での理論が不足している．本研究では，スタック木変換器に関する性質と表現力の調査を行い，スタック木変換器のクラス同士の表現力の違いを明らかにする．

ABSTRACT. Egisonは複数の結果を持つ非線形パターンマッチと、マッチャーを用いたユーザーによるパターンの拡張性をの両方を併せ持つパターンマッチ・システムを特徴とするプログラミング言語である。これらを実現するためにEgisonは特別な構文を持つため、型による静的検査の導入には、新たな型システムの設計が必要だった。我々はEgisonの型システムを設計し、その実装として型推論器をEgison上に実装した。また、その型安全性の証明のために[Egi, Nishiwaki 2018]の操作的意味論と今回設計した型システムをCoq上にFormalized Egisonとして実装した。今後の主な課題としてこの実装を用いた型安全性の証明がある。

ABSTRACT. 本研究は計算化学のHigh Performance Computingのためにプログラムを簡便に記述出来るドメイン特化言語（DSL）の提案を行うものである。計算の定義と最適化を分離することでコードのリファクタリングが容易なデザインを用いる。しかし従来のシステムでは、計算化学で用いるイレギュラーな配列に対応できない上、コードの記述が複雑になる問題があった。本研究では、計算化学で用いるデータ構造と計算式に応じた新しい型とReduction計算の記述を提案し、その問題点を解決している。新しい型は階層的なデータ構造を表す抽象機構であり、変数宣言時にデータの階層を読み込ませることでDSLのポインタとして活用することができる。これらを用いたuser adjustableなDSLのデザインを検討する。

ABSTRACT. プログラム合成とは，与えられた仕様を満たすプログラムを合成するタスクである．本研究では，プログラム合成手法の一つであるCEGISを拡張した層化CEGISを提案する．CEGISでは合成対象プログラムの入力例を反例駆動に集めながら候補プログラムの合成と，候補が仕様を満たすかの判定を収束するまで繰り返す．候補プログラムの合成では，これまで集めた入力例に対して出力の仕様を満たすようにプログラムのモデルのパラメータを決定する．しかし，CEGISにはモデルの表現力と汎化性能のトレードオフの問題があった．その問題を解決するために層化CEGISでは層化されたモデル族を導入し，unsat coreを用いた，モデルの表現力の自動調整を実現した．

ABSTRACT. 本研究では言語要素として版の概念を取り込んだプログラミング言語λVLの型システムに、型多相性と版多相性を導入する。λVLは、版によって実装の有無が変わる関数を使用したプログラムを許容し、そのようなプログラムが版において矛盾のない計算をすることを保証する。更に複数の版で無矛盾なプログラムは、必要に応じて適切な版を選択出来る。型多相性の導入によってモジュール機構が提供可能になり、版多相性によって特定の版に依存しないプログラムが書けるようになる。本研究は、２つの多相性の導入をカインドに基づく型システムの拡張によって行い、意味論を与え、健全性を証明した。

ABSTRACT. デザインレシピとは、プログラミングの手順を示したものである。このアイディアに基づいた環境は既にいくつかあるが、プログラムの構造の決定と網羅性の高いテストの作成へのサポートが不十分である。これらの問題を解決するために、本研究では、データ構造の分析を誘導し、その結果を使って場合分けやテストの作成を行う。また、今後の展望として、プログラム合成を用いたフィードバック機能について検討する。

ABSTRACT. 我々は、組込み機器上で動作するカスタマイズ可能なJavaScript仮想機械を実現する プロジェクトを進めており、ユーザの要求から必要最小限の機能を持つコンパクトな 仮想機械を構築することを目指している。 仮想機械コードの一部は型解析によって最適化が可能なドメイン特化言語で記述され ている。 既存の型解析は処理が高速である反面、十分な最適化が行われない可能性のある方法 で実装されている。 本研究では既存の型解析に加えて、最適化に直接関わる変数に関して詳細な型解析を 行う方法と全ての変数に関して詳細な型解析を行う方法の実装を行い、3通りの方法 の性能を評価する。

ABSTRACT. We propose a novel Lisp, Homoiconic Lisp, that has a simple but yet expressive meta-programming mechanism, designed to discuss a reasonably minimal condition of "program semantics" to give program semantics. A novel characteristic of the language is what we call "macro closure," a meta-level but also first-class function closure to manipulate program code. While the language's core is formalized as a simple extension of Landin's SECD machine and is implemented less than 1000 lines of C code, we can write a lot of programming language features (e.g., conditional expression, recursive function definition, and quasi-quotation) as user-defined programs.

ABSTRACT. Rustは高い性能と安全性を両立することを謳ったシステムプログラミング言語である。 Rustは所有権システムが潜在的に危険なメモリへのアクセスをコンパイル時に拒否することにより安全性を保証しているが、その制限はデータ構造や同期プリミティブ等の実装には厳しすぎる事が知られている。 そこで、Rustではunsafeによって所有権システムの制限を一時的に緩和することができるが、これは正しく用いられないとプログラムの安全性を損なってしまう。 この研究ではRustの特にunsafeプログラムに対して正当性を半自動的に検証するための枠組みを与え、開発者が継続的に検証を行っていくためのツールを提供する．

ABSTRACT. リアルタイムシステムは, システムの挙動に関して実時間制約をもつシステムであり, 実世界の幅広い分野で用いられる. 時間オートマトンはリアルタイムシステムの代表的なモデリング手法の一つであり, 簡潔にモデルを記述できるという特徴を持つ.

グラフ書き換えに基づくモデリング言語 LMNtal および そのモデル検査器 SLIM では, 並行システムのモデリングや状態空間構築, モデル検査などを容易に行うことができるが, 現時点ではリアルタイムシステム向けのサポートはなされていない.

本研究では, 時間オートマトンに基づくモデルを LMNtal でモデリングするためのフレームワークを提案した. また, 実際にシステムの状態空間構築を行う LMNtal プログラムを実装した.

ABSTRACT. イベント駆動プログラミングは，様々な分野で広く用いられているパラダイムである．Processingは，対話的で視覚的なアプリケーションのイベント駆動プログラミングに特化したプログラミング言語・環境であるが，低水準なイベント処理機能しか提供していないため，初心者には複雑な振舞いのプログラミングが難しい．本発表では，Processingプログラムにおけるイベント処理のユニットテスト手法を提案する．本手法は，イベント列を記述することでイベントハンドラを実行し，その結果得られるプログラムの内部状態が適切かどうかを判定するテストプログラムを記述できる．

ABSTRACT. モデル検査はプログラム解析の手法の1つであるが、スケーラビリティに問題がある。そこでプログラム検証問題の1つである到達可能性問題に着目し、入力プログラムの到達可能性に無関係のプログラム断片を除去することでこの問題を緩和する手法を提案する。これは注目しているプログラム地点への到達をエフェクトとして捉え、小林により提案された型情報に基づく不要コード除去を新しいエフェクトシステムによって拡張するものであるが、計算の意味の保存を保証せず到達可能性のみを保存する変換であり、不要コード除去よりも積極的な除去を行う。本発表ではこのプログラムスライシングのための規則を定式化する。

ABSTRACT. 高階関数や遅延評価などで再利用性を向上させることができる関数型プログラミングは重要である． 先行研究で，継続渡しスタイルを簡潔に記述できる関数型プログラミング言語Hatを提案した． 関数からの復帰や末尾再帰など様々な制御の流れが，直接スタイルでは暗黙に仮定されているが，継続渡しスタイルでは明示的に表現できるので，それを理解するためにHat言語は有用と考えられる． そこで，本研究では，学習者がHat言語の処理系をインストールすることなく，Webブラウザを用いて実行することを目的とし，その実行環境を設計し，実装した． 本発表では，本実行環境を用いて試作したHat言語のチュートリアルを実演する．

ABSTRACT. 関係データベース(Relational Database)の学習における主要課題の1つは，関係データベースの理論的背景となる関係代数(Relational Algebra)との関連の理解が難しいことである。これを解決するために，(1)Agdaを利用して関係代数を定式化した上で，(2)そこからSQL文を作成し実際のRDBで実行する ことを考えている。本ポスター発表では，既存のOSSをもとに発表者が改修したプログラムのデモを行う。定理証明支援系であり関数型プログラミング言語であるAgdaを使うことで，定義した数学的概念をプログラムとして実行することができる。この利点は，「コードは書けるがその理論は知らない，知りたい」という現場のシステムエンジニア向けの学習教材に有効ではないかと考えている。

ABSTRACT. 本発表では不動点算術の循環証明体系を提案する。通常の証明図は有限木だが、循環証明体系では証明図中にある種のサイクルをもつことができる。そのため有限の証明図の中で無限のパスを表現でき、帰納的定義を扱うことができる。帰納法についてのルールが単純な代わりに、証明図中の任意の無限パスに対し部分論理式の順序関係に依存したある種の条件を課す。我々はこの条件の決定可能性と、提案した証明体系の標準モデルにおける健全性を示した。また、拡張として高階算術論理の循環証明体系とその健全性を示した。

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

ABSTRACT. パターンマッチは、アルゴリズムの記述だけでなく、証明の記述も簡潔にすることが知られている。 実際、代数的データ型に対するパターンマッチは定理証明システムにも普及しており、Coq、Agda、Leanなどといったメジャーな定理証明システムのほとんどに組み込まれている。 本研究は、パターンマッチの対象を代数的データ型から非自由データ型（多重集合やグラフ、数式のように１つの定まった標準形を持たないデータ型）まで広げたEgisonのパターンマッチを証明の記述に応用する。 Egisonのパターンマッチを組み込んだ証明記述言語による素因数分解の一意性の証明を紹介し、Egisonのパターンマッチが証明の記述を簡潔にすることを示す。

ABSTRACT. あるプログラミング言語を用いて開発を行う際，ライブラリを取得するためにパッケージマネージャが広く用いられている．パッケージマネージャを利用する際，対象のパッケージが依存するパッケージの情報を再帰的に取得する必要がある．多くのパッケージマネージャでは，複数回のサーバへのリクエストを通じて依存するパッケージの情報を再帰的に取得した後，パッケージをダウンロードする．そのため，依存パッケージが多い場合，リクエスト回数が多くなり，パッケージの依存関係の取得時間が増大する．パッケージの依存関係の取得時間はパッケージダウンロード時間と比較して無視できない．そこで，本研究ではサーバ側で依存関係を事前に計算することで，リクエスト回数を減らし，パッケージの依存関係の取得時間を短縮するパッケージマネージャシステムを提案し，Scala言語で実装する．実装したシステムを用いて，npmの一部のパッケージを使って既存手法との比較実験を行い，依存関係の解決時間が短縮されることを示した．

ABSTRACT. strymonasは，モジュール性・記述性の高いfunctionalなストリーム処理を表す見かけの「パイプライン」から，安全で実行効率の高いimperativeなストリーム処理のコードを生成するライブラリ(EDSL)であり，どんなmap，filter，flatmap，zip，foldの組合せからなる「パイプライン」でも，中間ストリームはもちろん，多くの場合，いかなる中間データ構造も現れないコードを生成する特徴がある(stream fusion to completeness). 本研究の目的は，当初，POPL2017で発表されたstrymonasのリファクタリングを行うことで，その基本原理を明確にし，残留した中間データ構造を除去することである． 本発表では，リファクタリングの成果とベンチマークの結果を紹介し，実際にいくつかのストリーム処理のデモンストレーションを行う．

ABSTRACT. 分散並行システムのバグを静的に検出するのは困難である. 本研究では, 分散並行システムのバグの 静的検知を目指す. 並行システム特有のバグは, 検出や再現が困難である. なぜならば, 並行に動くシステム, プロセス, スレッド間の実行順序は, 一般的には非決定的だからである. 並行システムのバグの検知に関する研究 は今まで多く行われてきた. 従来の研究には, 共有資源とロックの関係に着目して, データ競合や競合状 態を検知するものがある. しかし, ロックセット方式の手法は, 分散並行システムには拡張できない. そ のため, 分散並行システムのバグの検出では, HB 関係に着目した手法が多い. だが, 従来の研究では, 動 的なアプローチが多く, 静的なアプローチはあまり行われていない. 動的なバグの検出は, 精度は高くな りやすいが, ソースコード全体を網羅的に探索できない. この研究で, 我々は, 分散並行システムにおけるバグを静的に検知する手法を提案する. 本手法では, 従来の Typestate 解析を応用する. また, ノード内及びノード間の HB 関係を解析する. Typestate 解 析と HB 関係をもとに, バグに到達し得るインターリーブを探索する. 提案手法を実装したものを合成 ベンチマークに適応した. その結果, 今回の予備実験の範囲に限るが, 実際に起こりうるバグを, 静的か

ABSTRACT. 分離論理によるプログラム検証の自動化のためには，帰納的述語を含む表明間の含意関係(エンテイルメント)を判定する必要がある． 　Tatsutaらは帰納的述語のcone条件を満たす帰納的述語を含むエンテイルメントに対して完全かつ決定可能な証明体系を提案し,Kimuraらはその証明体系をもとに自動証明器Cycompを実装した．しかし，Cycompはcone条件を満たすものしか扱えないため，分離論理のエンテイルメント判定器に関する国際競技会であるSL-COMP 2019 のベンチマークの問題ほとんどが扱えない． 　本研究では，Cycompに入力される帰納的述語とエンテイルメントをcone条件を満たすように同値変換する手法を提案し，それに基づく変換器を実装した．さらに，この変換器を利用し，SL-COMP 2019 によるCycompの評価を行った．

ABSTRACT. 量子コンピュータアーキテクチャ上では，CNOT ゲートは特定の量子ビットペアにのみ適用できる． この制約は coupling graph という，頂点として量子ビットをもち，辺で直接隣接する量子ビットペアに CNOT ゲートが適用できることを表すグラフで表現される． 本研究では Selinger らの量子ラムダ計算に依存型を導入し，与えられた制約のもとで型付け可能なプログラムを実行した際に CNOT ゲートが適用される量子ビットペアが必ず制約に違反しないことを保証する． また，型推論アルゴリズムにより，逆にプログラムが持つ coupling graph を抽出できる． 最後に，提案体系の型安全性および型推論アルゴリズムの健全性を証明する．

ABSTRACT. 関数リアクティブプログラミング（FRP）とはリアクティブシステムを宣言的に構築するプログラミングパラダイムである．組込みシステム向けFRP言語としてEmfrpがある． このEmfrpにおいて画像等のデータを扱うときに応答性が悪くなる可能性がある．一方で，GPUを搭載する組込みシステム向けのデバイスも出現した．そこで，本研究ではEmfrpで扱うと応答性が悪くなるようなサイズのデータを扱うために，GPUを利用できるような機構をEmfrpの後続言語のXFRPに導入する．

ABSTRACT. 組込みシステムの開発では非同期的な入力に対する応答処理と状態遷移に応じた振る舞いの変化が組み合わさることでプログラムが複雑になる．このようなシステムの記述を支援するため，本研究では小規模組込みシステムを対象とする関数リアクティブプログラミング（FRP）言語XStormを提案する．XStormは状態遷移を含むコンポーネントを記述するための言語機構を備えており，動的なメモリ管理を行うことなく実行時の振る舞いの変化を実現する．そのため，実行コードのメモリ使用量をコンパイル時に決定できる．提案する言語によって複雑な状態遷移を含むリアクティブなプログラムをモジュール化して記述できることを示す．

ABSTRACT. TypeScriptは既存のJavaScript実行環境上で動作する静的型付け言語である．実行環境にはその用途に合わせた独自のAPI（拡張API）が存在し，TypeScriptでは開発者が拡張APIの型定義ファイルをコンパイラに与えることで，拡張APIに関して型検査できる．しかしTypeScriptは拡張APIの型定義をプログラム中で切り替えられないため，プログラムに複数の実行環境のコードを混在させると不具合が生じる．そこで本研究では既存の型検査器を用いつつも，ブロックごとに型定義を切り替えて型検査できる補助ツールを開発し，この問題に対処する．

ABSTRACT. ユニタルクオンテール（完備べき等半環）は組(Q,≤,∨,⊙,1)でできている代数構造である。特に、最初の 3つが集合Xのべき集合P(X),包含関係,和集合であるようなユニタルクオンテールをべき集合クオンテールと呼び、さらにそのXが前順序,⊙が二項関係どうしの合成,1が恒等関係である例のことを関係的クオンテールと呼ぶ。現在、任意のべき集合クオンテールQからある関係的クオンテール P(R_Q)への埋め込みが見つかっている。このことから べき集合クオンテールとなんらかの条件下の前順序との間に相互変換があると考えられる。アプローチとして、これらを対象とする圏を考え、変換をその間の関手として定義することで関係を明らかにしていく。今回は、見つかった圏とそれらの間の関手について説明する。

ABSTRACT. 同値型は, ある型を持つ2つの項の同値性を型で表現する依存型の1種である. 本研究では, 依存型を持つ多段階計算の体系を同値型によって拡張する. 同値型で表現できる同値性は体系で同値な項同士のみであるという点で, 同値型は体系の同値に密接に関連する. 簡約はYuseらの方法に倣い, ステージに対応する整数インデックスで拡張することで, 適用可能な簡約規則を制限しており,同値性の定義に関しても, この簡約に対応するため, 整数インデックスに関して拡張した. 最後に, 体系の安全性,強正規化性,合流性を示したあと, アルゴリズム的型付けを導入し, 宣言的型付けに対する健全性と完全性を証明する.

ABSTRACT. 最近のブロックチェーンにはスマートコントラクトというプログラムを動かす仕組みがあり、取引の自動化などに使われている。しかし、スマートコントラクトにバグがあると 莫大な金銭的損失が生まれてしまうことがあり、実際にEthereumというブロックチェーンではスマートコントラクトのバグにより50億円相当の暗号通貨が盗まれる事件が発生している。 本発表では、Tezosというブロックチェーン上で動くスマートコントラクト言語Michelsonに対して、 データについての様々な性質を型で表現できる篩型(refinement types)という仕組みを導入し、型システムによってスマートコントラクトの安全性を検証する手法を提案する。

ABSTRACT. 静的型検査はプログラムの仕様を網羅的に検証できる反面，型として表せない仕様は検査することができない．一方アサーションは，網羅的な検査はできないものの，任意の述語を用いて値が満たすべき性質（不変条件）を表現することができる．アサーション内に書かれた述語は，プログラマがデータに対して想定する性質や役割を表す．そのため，変数が満たしたアサーションの述語を求めることで，変数が果たす役割も明らかにすることができると思われる． 本研究では，静的に計算したデータフローに沿ってアサーション内に書かれた述語を網羅的に伝播させることで，変数のとる値の役割を説明するような述語の集合を求めるデバッグ支援ツールを提案する．

ABSTRACT. 最短経路問題は，重み付きグラフ上で与えられた2頂点を結ぶ経路の中で重みの総和が最小のものを求める問題である。最短路を見つける問題に還元される問題は多い。例えば，道路の経路探索や、避難経路選択など，さまざまな最短経路問題がある。最短経路を探索する手法の一つとして遺伝的アルゴリズムがある。本研究では遺伝的アルゴリズムを最短経路問題に適用するのに適した交叉手法を提案する。従来手法はランダムに交叉点を選び交叉する。そのため部分的な最短経路が遺伝しない可能性がある。本研究では２つの染色体から同じ遺伝子（ノード）2個のペアを２つ探し出す。その2つの遺伝子の間で適応度を計算し、値が小さい区間に対して二点交叉を行うことで次世代に部分的な最短経路を遺伝させる。これにより、世代数が減少すると、処理されるデータの量が減少し、最短経路探索時間が短くなることが期待される。

ABSTRACT. 解集合ソルバーは，一階論理に基づいて記述された規則から，安定モデル意味論に基づいた解集合を求めるシステムである． 近年，SAT技術を利用した解集合ソルバーが開発され，性能が向上している． 様相命題論理とは命題論理の拡張であり，様相演算を用いることで必然性と可能性などを表現できる論理である． 本発表では，様相命題論理をタブロー法に基づいた推論規則に変換し，可能世界を順次追加する手法で充足可能性判定を行う． 特にヒューリスティクスを用いて追加する可能世界を選択することで，SATソルバーを用いた既存手法よりも 優位性が見られる場合があることが判明した．

ABSTRACT. ソースコードから特定の部分を抽出したいことは頻繁にある.「コードを共通化するリファクタリング作業のために、あるコードに似た部分を洗い出したい」「自分の知らない記法について by-example で学習するために、あるコードに似た部分を探したい」「ドキュメントが整備されていないライブラリの使い方が正しいか確認するために、自分の書いたコードに似た部分を確認したい」である. 本発表では "トークン列に対する曖昧検索" を実現するに当たって必要な議論を行う. 具体的には (1) プロトタイプアルゴリズムの紹介, (2) 他のソースコード技術との比較, という2点についての議論である. 現在研究は初期状態であるため, ポスターという形式で対話的に議論することで研究を発展させることを見込んでいる.