ABSTRACT. 伝統的なオートマトンや形式文法はさまざまな方法で拡張されている．そのような拡張の一つとして，レジスタをもつモデルについてお話しする．データ値の無限集合を一つ仮定しておき，オートマトンや形式文法にデータ値を記憶するレジスタを導入する．表現能力をほどほどに抑えるため，レジスタに記憶されたデータ値に対しては比較演算（典型的には等号判定）しか許さない．このような考え方で拡張されたモデルであるレジスタオートマトンとレジスタ文脈自由文法を取り上げ，その基本問題の判定可能性や計算量，言語演算に対する閉包性などを紹介する．次に，拡張モデルである凍結子付き時相論理，２変数１階論理を紹介する．関連する計算モデルとして，重み付きオートマトンと形式級数，時間オートマトン，ベクトル加算系などにも触れる．時々寄り道をして，プログラム検証や情報流解析，厳密学習などへの応用についてもお話しする．

ABSTRACT. 差分解析はプログラムの変更前後での振る舞いの変化を特定する技術であり，予期せぬ振る舞い変化の検出や回帰テスト等に有用である．既存の差分解析手法は，プログラムの入力に起因する入力空間の探索は行うが，イベント処理の順序に起因するイベント空間を考慮していないため，イベント駆動コードの差分解析には不十分である． そこで，本研究では入力×イベント空間における差分解析手法を提案する．提案手法では膨大な入力×イベント空間を効率良く探索するため，汚染解析やDPORによりイベント空間において探索不要なパスの枝刈りを行う．同時に，コードの差分・出力とのCDG上での距離を用いて差分の影響が出力に現れるよう探索パスを誘導する． 実験では，現実のサーバーサイドNode.jsアプリケーションを対象に，プログラムの振る舞い差分検出の精度と探査パス数による効率の評価により，提案手法の有効性を確認する．

ABSTRACT. プログラムがスタック領域上で時間的メモリ安全であるとは、プログラムが任意の入力に対して実行されたときに、スタックフレーム上に構築されたオブジェクトを指すポインタが、そのオブジェクトの寿命の範囲を超えて生存しないことを意味する。本研究はこの種のメモリ安全性を保証する静的解析手法を提案する。本手法はデータフロー解析によりプログラムの各時点でのpoints-to関係を列挙し、不正に長い期間生存するポインタが存在し得るかどうかを検査する。本手法は解析に型情報を用いず、関数定義ごとに独立して適用されるため、ポインタ整数間の変換を含む低レベルなプログラムや、ソースコードが一部しか入手できないプログラムの解析にも用いることができる。本研究はさらに、本手法をLLVM IRに対する解析器として実装し、本手法の精度を評価した。

ABSTRACT. 通常の論理や普遍代数では，有限項のみを対象としている．一方，有限項の一般化として無限項があり，その中でも，有限種類の部分項しか持たない項を正則項という．正則項を対象とした書き換えが，Corradini \& Gadducci(1998)や青戸 \& Ketema(2012)によって考えられている．正則項書き換えは，書き換え位置の集合が正則集合となるような書き換えを考えるという特徴がある．また，正則項は有限表現を持ち，書き換えに関する基本的な性質が計算可能となる．本論文では，交換律の規則による正則項書き換えについて考察する．具体的には，書き換え位置の集合を表す有限オートマトンと有限表現上の書き換えステップとの関係を明らかにし，逆向きの書き換えを行う有限オートマトンの構成法や2ステップの書き換えを行う有限オートマトンの構成法を与え，その正しさを証明する．

ABSTRACT. 文字列の検索等に広く用いられる正規表現マッチングはその多くがバックトラックに基づくアルゴリズムで実装されており，対象文字列の長さに対して線形時間でマッチングを完了できない場合がある．これを事前に検知するために，マッチングに要する計算量を静的解析する手法が複数の先行研究によって提案されている．本研究では先行研究を拡張し，先読みや先頭/末尾のマッチなど，現実のソフトウェアで使用されている拡張された正規表現に対しても解析が行える手法を提案する．さらに，既存の解析アルゴリズムを高速化し，より実用的な速度で解析を行える手法を提案する．そして，これらの改良を施した計算量解析のツールをScalaで実装し，既存の実装よりも多くの正規表現が解析できることを実験により確認した．

ABSTRACT. 投機的実行や深いメモリ階層などで計算機システムが複雑化するに伴い，プログラムや言語処理系の性能評価を適正に行うことが困難となっている．例えば，配置のみ少し異なるコードの実行性能が大きく異なるといった問題がある．このようなコード配置効果を考慮して総合的，統計的な性能評価を行うため，コード配置のみ異なる多数のプログラムを生成して性能を測定するコードシェーカという性能評価システムが提案されている．しかし，与えられたアセンブリプログラムを対象としてラベル直前などの実行しない箇所に境界整列の代わりにランダムなパディングを行う仕組みであるため，JITコンパイルを行う仮想計算機（VM）には適用できない．本研究では，Java VMのJITコンパイラを作り変え，同様な測定を行うことで，JITコンパイルを行うJava VMでもコード配置効果が見られることを確認した．

ABSTRACT. 近年IoT(Internet of Things)技術が注目を集めている．eJS(embedded JavaScript)プロジェクトでは，IoTアプリケーション開発にJavaScriptを利用可能とすることで，開発の複雑さ等の排除を目指している．eJSプロジェクトでは，計算資源が限られるIoT機器上でも効率よく動作するよう，機器や対象アプリケーションに合わせたカスタマイズが可能なJavaScript仮想機械(eJSVM)を提供する．本論文では，より効果的に動作するeJSVMが提供できるよう，64ビット環境向けと32ビット環境向けのデータ構造を選択可能とするカスタマイズ項目と，対象アプリケーションと相性の良いごみ集めアルゴリズムを選択可能とするカスタマイズ項目のふたつを実現した．また，ベンチマークプログラムを用いた評価実験を通して，これらのカスタマイズ項目の追加により，従来よりも効果的に動作するeJSVMを提供できることを確認した．

ABSTRACT. 本発表では，SML#の新たなマシンコード生成方式の構想について述べる．SML# は，Standard MLを包摂しながら，マシンネイティブなデータ表現，正確なゴ ミ集め（GC），および分割コンパイル方式を採用する関数型言語である．これ らの特徴を実現する上での実装上の主要な課題は，多相関数を多相的な性質を 持つマシンコードにコンパイルすることにある．型主導コンパイルに基づくビッ トマップコンパイル方式はこの課題を解決する基礎理論を与えているが，実装 技術についてはスタックフレームを巧みに制御することを示唆するに留まって おり，その実装はコード生成器とコンパイラフロントエンドの強い結合を招き， LLVMなど最先端のコンパイラ基盤の利用を難しくする．本発表では，SML#コン パイラ開発におけるこの課題へのこれまでの取り組みを概観した後，これまで のアプローチが抱える問題点を整理し，それらを克服する新たなコンパイル方 式について述べる．

ABSTRACT. Hylomorphism を用いたプログラム運算は、適用範囲が広く有用であり、その正しさを検証するためのシステムが望まれる。定理証明支援系 Coq を用いて運算を検証するシステムはいくつか知られているが、hylomorphism およびその運算規則を使いやすい形で形式化することは困難であり、著者の知る限り未だ実現されていない。その困難さは、Coq においては帰納的データ型と余帰納的データ型が区別される一方、hylomorphism はこれらが同一視されるような条件の下で定義されるというギャップにある。本研究では、このギャップを回避しつつ形式化するための技術として、遅延モナドおよび再帰的余代数の利用を検討し、例を用いてこれらの長所や短所を議論する。

ABSTRACT. On formalizing nontrivial mathematical theorems with proof assistants, it is necessary to have a good infrastructure to support the users. The hierarchy of mathematical structures that allows for the sharing of notations and theories, and makes subtyping of structures implicit, is a key ingredient of the infrastructure. The packed classes method is a generic design pattern to define and combine mathematical structures in a dependent type theory with records. The Coq proof assistant has mechanisms to enable automated structure inference and subtyping with packed classes; that is, implicit coercions and canonical structures. In this paper, we propose a thorough analysis of the packed classes method, in particular some invariants of hierarchies that ensures the modularity of reasoning and the predictability of inference with packed classes, and propose tools to support its large scale deployment by checking those invariants.

# This submission will be simultaneously submitted to IJCAR 2020. # 本投稿は IJCAR 2020 に同時投稿予定です。

ABSTRACT. 定理証明系言語で証明を書くとき、場合分けが多くなることや、定義を少し変更しただけで残りの証明の大部分を変更しなければいけないことがある。これを解決するために、Coq などの言語では自動証明のための環境が整っており、Agda でもそのような自動証明ができるのが望ましい。 現在、Agda では、Idris の Elaborator Reflection に影響を受けた新しい Reflection API が提供され始めている。この Reflection API はまだ開発途中の段階だが、証明の型チェック中に証明の型の情報を読み取ったり、書き換えたりすることができる。 本稿では、単純型付きλ計算に対する CPS 変換の正当性の証明を例にとって、Agda の Reflection API で自動証明をおこなった模様を報告する。具体的には、λ計算の代入と簡約を自動でおこなうタクティクスを作成することで、単純な証明の部分を自動化することができた。また、Selective CPS 変換の正当性の証明のような大規模な証明の一部を自動化する。

ABSTRACT. ステッパはプログラムの実行過程を見せるツールである。これまで様々な言語に対するステッパが作られてきたが、shift/reset や algebraic effects といった継続を明示的に扱う言語機能をサポートするステッパは作られていない。継続を扱うプログラムの挙動を理解するのは困難なので、そういった言語に対応したステッパを作ることが本研究の目的である。 ステッパは簡約のたびにその時点でのプログラム全体を出力するインタプリタなので、実行している部分式のコンテキストの情報が常に必要になる。継続を扱うような複雑な機能を持つ言語を対象にしたステッパでは、コンテキストがどのような構造をしているかが自明でない。そこで、通常のインタプリタ関数をプログラム変換することで機械的にコンテキストの情報を保持させてステッパを実装する方法を示し、実際に型無しλ計算と algebraic effects から成る言語に対するステッパを実装する。

ABSTRACT. Algebraic effects and handlers are a powerful abstraction mechanism to represent and implement control effects. In this work, we study their extension with parametric polymorphism that allows abstracting not only expressions but also effects and handlers. Although polymorphism makes it possible to reuse and reason about effect implementations more effectively, it has long been known that a naive combination of polymorphic effects and let-polymorphism breaks type safety. Although type safety can often be gained by restricting let-bound expressions---e.g., by adopting value restriction or weak polymorphism---we propose a complementary approach that restricts handlers instead of let-bound expressions. Our key observation is that, informally speaking, a handler is safe if resumptions from the handler do not interfere with each other. To formalize our idea, we define a call-by-value lambda calculus that supports let-polymorphism and polymorphic algebraic effects and handlers, design a type system that rejects interfering handlers, and prove type safety of our calculus.

ABSTRACT. 双方向変換はモデルやコードなどの成果物間の同期が求められるモデル駆動工学などでの利用が期待されている。双方向変換は上記のような一対一の情報源間の同期の他、多対多の同期の研究も盛んであり、自律的な主体の保持するデータ間の同期もその一例である。このような多方向変換の様々な場面で、順方向変換のrange同士の接続(co-targetial composition)等の双方向変換の組み合わせに帰着されることが知られているが、値から値への関数でモデル化される状態ベースの双方向変換の合成には問題が指摘されている。本発表では、発表者等が取り組んで来たグラフの双方向変換を中心に、合成を容易にするための漸進化手法について述べる。

ABSTRACT. 近年x86アーキテクチャのSIMD命令を活用し、スカラー命令より良いパフォーマンスは可能である。しかし、低レベル命令として、SIMD命令のC言語による組み込み関数は引数の型情報を持たないため、型安全性は保証できない。本研究はOCamlの強い型システムを利用し、経験を持たない一般のプログラマも書ける型安全性持つSIMD命令を利用できるコードの自動生成を目指している。

ABSTRACT. 帰納的に定義される対象における定理(始代数上の定理)を帰納的定理と呼び，等式論理における帰納的定理の証明手法として書き換え帰納法や潜在帰納法が知られている．一方，余帰納的定理という概念もあり，これは帰納的定理の圏論的な双対概念(終余代数上の定理)として形式化される．また，余帰納的定理の証明手法として文脈帰納法や循環余帰納法が知られている．しかし，書き換え帰納法や循環余帰納法は始代数や終余代数を直接には用いておらず，それらの間の関係も調べられていない．本発表では，帰納的定理と余帰納的定理に関する定理証明問題や定理証明法について，圏論を用いて考察する.

ABSTRACT. This is a work presented in LICS 2019. Bisimilarity as an equivalence notion of systems has been central to process theory. Due to the recent rise of interest in quantitative systems (probabilistic, weighted, hybrid, etc.), bisimilarity has been extended in various ways: notably, bisimulation metric between probabilistic systems. An important feature of bisimilarity is its game-theoretic characterization, where Spoiler and Duplicator play against each other; extension of bisimilarity games to quantitative settings has been actively pursued too. In this paper, we present a general framework that uniformly describes game characterizations of bisimilarity-like notions. Our framework is formalized categorically using fibrations and coalgebras. In particular, our characterization of bisimilarity in terms of fibrational predicate transformers allows us to derive codensity bisimilarity games: a general categorical game characterization of bisimilarity. Our framework covers known bisimilarity-like notions (such as bisimulation metric) as well as new ones (including what we call bisimulation topology).

ABSTRACT. It is well-known that the linear-non-linear model (LNL model) introduced by Benton is a categorical model of intuitionistic linear logic (and hence linear lambda-calculus), and gives a mathematically elegant formulation of the exponential modality. It based on an adjunction between a cartesian closed category (CCC) and a symmetric monoidal closed category (SMCC), and reflects an intuition that there is a relationship between intuitionistic logic and intuitionistic linear logic. In this poster presentation, we consider its modal extension; namely, we discuss an LNL model in a modal logical setting, replacing the base categories with modal logical categories, and some technical difficulties will also be mentioned.

ABSTRACT. IOTなどで用いられるような小型デバイスで高機能なプログラム言語を使用する場合、ヒープが不足するようになる。 その場合、通常のメモリに加えて不揮発性メモリもヒープとして使う方法を取ることができる。 しかし、不揮発性メモリは書き込み回数に限度があるため、いずれ書き込みできなくなる。 この問題を解決するため、不揮発性メモリの性質に特化したメモリ管理機構を提案する。 今回開発したメモリ管理機構では、ページングアルゴリズムの改良とガベージコレクション時にオブジェクトを都合の良い場所に置くことで、不揮発性メモリへの書き込み回数を抑えることを実現した。

ABSTRACT. In typical implementation of JavaScript virtual machines (VMs), an object comprises two parts: an object body and an external array, which contains the values of fields. If a field is added, the VM reallocates the external array. Thus, access to a field involves an indirection. We addressed this problem by estimating the final set of fields of objects at their allocation site based on information collected by the garbage collector. Objects are allocated with sufficient room to allocate fields in their object bodies. We present the implementation of this mechanize in eJS JavaScript engine.

ABSTRACT. Universeフレームワークは、初学者向けにゲームプログラミングをサポートするフレームワークであり、Unixモジュールのプロセス間通信を利用した通信ゲームの作成が可能である。本研究では、初学者にとってより身近なブラウザ上で動く通信ゲームをWebSocketを用いて実装した。WebSocketのために取り入れたsocket.ioというモジュールはNode.jsから利用できるため、JavaScriptで書いたコードをOCamlに変換した。今回の発表では、通信ゲームの状況と実装について報告する。

ABSTRACT. Haskellを対象とするトレース手法としてHatLightが提案されている． HatLightは，関数の呼び出しと計算結果を保持するようにHaskellプログラムを変換してトレースを行う． また，トレース結果はARTと呼ばれる有向グラフで保持されるため，トレース結果をさまざまな形式で表示可能である． しかし，ARTを生成するためには，トレース対象のプログラムが参照しているライブラリの変換も必要となるため，多数のライブラリを参照している場合にトレースが困難となる． 本論文では，HatLightの課題の解決を目的とし，参照しているライブラリの変換を必要とせず，その結果の値のみをARTに記録することで構造を維持する手法を提案し，実装について報告する．

ABSTRACT. Hylomorphism を用いたプログラム運算は、適用範囲が広く有用であり、その正しさを検証するためのシステムが望まれる。定理証明支援系 Coq を用いて運算を検証するシステムはいくつか知られているが、hylomorphism およびその運算規則を使いやすい形で形式化することは困難であり、著者の知る限り未だ実現されていない。本研究では、この形式化を実現する案として、遅延モナドを用いた手法を検討する。（カテゴリ1の同発表者同タイトルの発表と同内容の発表を予定しているが、本ポスター発表では議論を重視し、形式化の詳細や理論の細部を示す予定である。）

ABSTRACT. Agda による プログラムの証明は、何千行にもわたることもある。また、中には、自明で機械的に証明を行いたい部分もある。そこで、機械的できる部分は Agda で証明を自動生成をしたいと考えた。Reflection API は Agda でメタプログラミングが行える機能である。この reflection の機能は あまり広く知られていない。そこで、reflection を使って証明を自動生成するための関数 macro を体系的に定義をする方法を提示し、さらに、Equational Reasoning で証明する方法について提示する。本研究では、足し算の証明の自動生成、λ計算の簡約関係の自動生成の方法と結果を報告する。

ABSTRACT. マルチスレッドプログラミングにおいては，他のスレッドのメモリアクセスを実行時に観測したときの順序がソースコード上の順序と異なって見えることがある．どのような入れ替わりが発生しうるかはメモリモデルによって規定されるが，弱いメモリモデル上では直感に反する挙動も許容されることがあり，正しく動作するプログラムを人間の注意力のみに頼って書くことは困難である．そのため弱いメモリモデル上でプログラムが正しく動作するかを効率良く検査するステートレスモデル検査手法が活発に研究されている．しかしその性能評価は小規模なプログラムを用いて行われることが多く，実用規模のプログラムが現実的な時間内でモデル検査できるかどうかは知られていない．そこで我々は最先端のステートレスモデル検査器であるGenMCを用いてC11メモリモデル上で実用規模の並行Cライブラリの検証を試みた．本発表ではその検証過程において発生した問題と，その解決方法に関する知見を共有する．

ABSTRACT. ポインタの複製などを持つ低レベルなプログラムは検証が難しいことで知られている。この解決のために、Toman et al.は所有権と篩型を用いた健全な型システムを導入し、それに基づいたConSORTという自動検証器を開発した。これは非自明なプログラムを検証できるが、現在の実装においては型付け不能な場合には意味のある出力をしない。そこで我々は型付け不能なプログラムに対して反例を生成する方法を提案し実装した。ConSORTの型推論には二段階あることや型システムの非完全性を考慮し、三種類の反例の概念を導入し生成方法を与える。本手法に基づきConSORTに反例生成器を組み込み、その有効性を確認した。

ABSTRACT. 本発表では，動的型付け言語であるJuliaで書かれたプログラムに対する静的解析器として，プログラムを型レベルで抽象解釈することによりバグを検出する型プロファイラを提案したい．

この型プロファイラは，プログラムの抽象解釈に，JuliaのJITコンパイル機能の核として既に実装されている型推論ルーチンを利用することで，抽象解釈によるプログラム解析において問題となりやすいスケーラビリティを保ちつつ，実用的なエラー検出能力を持つことを目指して作成した．

その設計や性能について，昨年のPPLでも発表されていたruby-type-profilerとの比較も行う．

ABSTRACT. Most computer programs including libraries and software applications use version numbers as identifiers. Build tools and package installers such as Gradle and Maven manage dependencies between programs using their names and version numbers. Build tools will fail if two or more versions of any particular program is needed. Although this restraining, such behavior is necessary because the names of exported classes, functions, or variables may overlap among multiple versions of one program. We propose programming with versions to overcome this restraint. In this paradigm: (1) exported classes, functions, and variables are distinguished by their names and version tags; (2) programs are built in both contextually polymorphic and contextually monomorphic manners. We introduce a new Java-based programming language BatakJava to illustrate this proposal. BatakJava allows classes to have different sets of fields and methods among versions.

ABSTRACT. プログラムがスタック領域上で時間的メモリ安全であるとは、プログラムが任意の入力に対して実行されたときに、スタックフレーム上に構築されたオブジェクトを指すポインタが、そのオブジェクトの寿命の範囲を超えて生存しないことを意味する。本研究はこの種のメモリ安全性を保証する静的解析手法を提案する。本手法はデータフロー解析によりプログラムの各時点でのpoints-to関係を列挙し、不正に長い期間生存するポインタが存在し得るかどうかを検査する。本発表では、本手法をLLVM IRを対象として実装した解析器のデモを行う。

ABSTRACT. We plan to present a computation graph-based computation model that is composition friendly, in the sense that smaller computation graphs could be composited into larger ones meaningfully.

Computation graphs have long been used as computation models. They usually have intuitive semantics and are natural to visualize, while being versatile to model significantly complicated calculations.

Yet computation graphs are traditionally created or generated as a whole instead of being mechanically compiled or "composited" from smaller parts that make individual sense. This is in contrast to the now-common structural programming, where programmers write small pieces of code of programs that individually implement certain functionality and only then have a "compiler" program to assemble them automatically into a larger piece of program to be executed. This property of structural programming is commonly attributed as *composability* and widely appreciated.

In this presentation, we will present a computation model *2flow*, that is a computation graph-based model and also enjoys meaningful composability.

2flow is developed as part of the authors' previous company's attempt to create a domain-specific language (DSL) for accountants in certain private sectors who on a daily basis perform complicated and intricate calculations which could actually be decomposed into small and concise rules. Using a computation graph based model to support such a DSL allows us to provide the ability of visual inspection of the calculation rules and helps ease the usage of the system by non-programmer domain experts.

ABSTRACT. Combinatrial t-way testing is a test data sampling technique, whose effectiveness has been shown by a number of empirical studies. Combinatrial t-way test generation is a central subject in the field of combinatrial t-way testing, and various algorithm have been proposed in the literature. We attempt to develop a new algorithm for combinatrial t-way test generation using General-Purpose computing on Graphics Processing Units (GPGPU). In this poster, we report the current research-in-progress of this work.

ABSTRACT. 継続とは、計算過程のある時点における残りの部分を意味する概念である。関数型プログラミング言語であるSchemeなど、一部の言語は継続を明示的に取り出して扱う機構を持っている。 LMNtalはグラフ書き換え言語のひとつである。多くのプログラミング言語とは異なり処理が並行性を持つため、継続を一意に定義することが出来ない。 本研究では、LMNtalグラフの構造を計算過程とみなすことによって継続の概念をLMNtalに導入した。またその定義に基づいて継続を扱う機構を実装し、例題を用いて実用性を確認した。

ABSTRACT. Lift ILはGPGPUプログラムのための配列指向の中間言語である。Lift ILには動的に長さが決まる配列を表現できないという問題がある。 本発表では、存在型を用いて配列型の長さを隠蔽することで、Lift ILにおいて動的長配列を扱う方法を提案する。 その際、型から配列長を隠蔽・展開する操作を適切な場所に挿入する必要があるが、それらの自動挿入方法も提案する。 この提案に基づいて、Lift ILのコンパイラを作成し、その上でフィルター関数を実装した。 さらに、Project Euler問題集を用いて、拡張したLift ILコンパイラで動的長配列を扱うプログラムが記述・コンパイル・実行できることを確かめた。

ABSTRACT. νHFLZは最大不動点と整数算術を含む高階論理の一種である。小林らは高階関数型プログラムの安全性検証がνHFLZ妥当性検証に帰着できることを示した。従ってνHFLZ自動妥当性検証器は、高階関数型プログラムの安全性検証に利用できる。BurnらはνHFLZ妥当性検証と等価な高階CHCの充足可能性問題のための篩型システムを提案し、それに基づくソルバを実装した。この手法は述語抽象化と高階モデル検査の組み合わせによる手法に比べ高速だが検証能力が弱い。我々は健全かつ完全な部分型規則を新しく導入し、検証能力を強化する。さらに提案する型システムに基づく自動妥当性検証器を実装し、実験からその有効性を確認した。

ABSTRACT. 関数リアクティブプログラミング(FRP)とは，時間変化する値を抽象化し，継続的に入出力を行うシステムを設計するプログラミングパラダイムである。Emfrpは組込みシステムを対象としたFRP言語である。組込みシステムにおいては，アクチュエータの想定外の動作による故障を防ぐことが課題となっている。本発表では，Emfrpのサブセット言語であるminiEmfrpによって実装された，センサ1つのみを入力とする関数リアクティブシステムを対象として，アクチュエータが正常に動作するための制約から，それを満たすような入力センサの仕様を推定する手法を提案する。

ABSTRACT. 我々は，ワークスティールによる動的負荷分散を行うタスク並列言語Tascellを開発している．Tascellの特徴の一つとして，分散環境で計算ノードを跨ぐワークスティールにも対応するという点がある．しかし，分散環境での効率的な計算のため，Tascellプログラマはスティール時のタスクの入力や結果データの授受等の処理を明示的に記述する必要があり，たとえば同種の並列言語であるCilkなどと比較してコードが煩雑になるという問題があった．そこで本研究では，Tascell言語の並列構文を拡張し，生成されたタスクの入力，および結果の受け取り先に相当する局所変数を宣言的に記述するだけで，これらのデータ授受処理を定義できるようにした．

ABSTRACT. 継続とプログラムの対称性をもつ計算体系の一つに、Filinskiが提案し浅井らが整備した対称λ計算(SLC)がある。SLCは上の双対性に加えてさらに「関数」の中立性をもつ。「関数」とは、プログラムに作用する通常の関数であると同時に継続と結合して継続の一部となりうる両義性を持った構文論的対象であり、中立性とはこの性質を指す。SLCはカット相当の型規則が最後の1箇所のみに許されている体系であり、継続・「関数」・プログラムの結合の入れ子構造は形成されなかった。本発表では、この制限を外したSLCの拡張 入れ子対称λ計算(NSLC)を定義し、カット除去の手法を用いてCBV NSLCおよびCBN NSLCの停止性を示す。NSLCによる古典論理の計算的解釈も述べる。

ABSTRACT. GPGPU (general purpose computing on graphics processing units) is one of the economical methods of parallel programming. However, in order to obtain high performance, the programmers must write in a low-level programming language, such as C, with paying attention to memory allocation. We propose Sanajeh, a DSL (domain-specific language) in Python that compiles programs written with Python objects into GPGPU code. Our proposal consists of two parts, the first one is a core language which is based on the Single-Method Multiple-Objects (SMMO) model. The second one is a library for high-level parallel programming patterns such as parallel graph and tree algorithms. This poster presents an implementation of the core language by translating Python programs into C++/CUDA code with DynaSOAr, which is an efficient parallel memory allocator. It also discusses the design for the high-level parallel library by using Barnes-Hut simulation as an example.

ABSTRACT. Moggiのsimple metalanguageの一部を改変することで， ある種の計算作用を持つ複数の新しい計算モデルが得られることが知られている． 本研究では，代数的なモノイド作用の同変写像に対応する，圏論における同変関手が それらの計算モデルのうちの１つの圏論的モデルになっていることを示し， その上でその計算モデルの性質を意味論的に調べるための手段として 同変関手についての圏論的貼り合わせを記述する． また，その系として上述の計算モデルについての論理述語を提案する．

ABSTRACT. LMNtalはグラフ構造をルールを用いて書き換えていくことで計算を表現する言語である。コンパイラで独自設計の中間命令列に変換された後、仮想マシン上で実行される。

先行研究でコンパイル時にルールの書き換え前後で共通するノードを再利用し数学的根拠に基づく安全な方法でエッジを再構築するよう中間命令列が最適化された。しかしルールに実行時に動的に決まる部分グラフが含まれると最適化できない制約があった。

本研究ではノードの再利用を拡張し、実行時に動的に決まる部分グラフについても再利用を検討する。仮想マシンの拡張と新たなコンパイル時最適化のアルゴリズムを設計し、例題プログラムが従来より高速化することを確認した。

ABSTRACT. パーサコンビネータで使用される先読み付き文脈自由文法を対象に理論的な研究を行なった。 同じくパーサコンビネータで使用される解析表現文法は先読み付き文脈自由文法の一部分とみなすことができる。 まず、先読み付き文脈自由文法の表示意味論的な定義を与えた。 これは、先読み付き言語とブール文法で使われる空集合からの反復の極限を組み合わせることにより行った。 解析表現文法では操作的意味論的な定義が与えられていたが、それらよりも数学的に扱いやすく、左再帰を含む文法に適切な定義を与えることが可能になる。 次に、先読み付き文脈自由文法の微分を与えた。 文脈自由文法の微分を独立に形式化し、先読み付き正規表現の微分と組み合わせることにより行った。 木を用いずに所属判定ができるという特徴を持つ。

ABSTRACT. Many popular scripting languages like Python share a great reputation for their flexibility giving the code a large degree of polymorphism and high abstraction. With the urge of static analysis in dynamic languages, Python has been support- ing type annotations as an optional way to possibly lift itself to a static level. However, manually writing type annotations in order to let a static checker give a deep, satisfactory analysis is obviously burdensome. Besides, they are not so heavily used in major applications. Meanwhile, unit testing has been a popular trend among dynamic languages as an alternative to static typing for years. In this work, we want to type Python programs using type information available during unit testing. The captured type signatures can be used to support static analysis so that the program can be enforced with type safety. While from a theoretical point of view, abstracting ambiguous, complex types from concrete ones obtained from unit tests is evidently not complete, we believe that even such a weak type system can be still valid for typing Python programs. We collected open-source, real-world Python repositories as sample programs and did a small-scale experiment. The type information is gathered during unit testing and guides type-check the programs. The results suggest that typing a program via unit testing is fairly lightweight compared with statically writing type annotations, but at the same time a remarkably effective approach carry static typing to highly dynamic languages.

ABSTRACT. 本発表では Ruby から Javascript を呼び出す FFI の開発に向けて，我々が遠慮のかたまり問題と呼ぶ問題について論じる．Javascript の V8 VM は複雑であるため，ガベージコレクタの改造は困難であり，自身のヒープ領域だけを管理させる設計が望ましい．このように複数のコレクタが個別の領域を管理する環境では，リモートリファレンスによって他領域から参照されるオブジェクトは管理を相手側のコレクタに任せ，自分では触らないという方針が一般的である．しかし，この方針にはリモートリファレンス同士の循環が回収できないという問題がある．本発表ではこの問題を遠慮のかたまり問題と呼び，その解決方法について論じる．

ABSTRACT. 関数リアクティブプログラミング（FRP）は，時間に依存して値が変化する時変値における依存関係を，副作用のない計算を用いて宣言的に記述するプログラミングパラダイムである．本研究は，Deep Embeddedな内部DSLとしてのFRP言語LRFRPとその実装を提案する．ホスト言語として用いるRustは静的なメモリ安全性の検査を提供し，さらに組み込み開発への応用も進んでいる．そのためLRFRPはC/C++をベースとしたFRP言語に比べ，よりメモリ安全な組み込み開発を提供することも期待できる．

ABSTRACT. Due to the increase in cross-platform applications and the transplantation of software, repetitions of functionality in different programming languages become unavoidable. These repetitions of similar code in different programming languages are known as cross-language code-clones. Detecting cross-language code-clones implemented in different programming languages is vital for tasks like version control and bug fixing for cross-platform applications. However, cross-language code-clones are usually syntactically different from each other which makes them difficult to be detected. Many studies have already been conducted in this area, some of them work on abstract syntax tree (AST), a syntactical structure of source code, which may share some similarity between code-clones despite the difference in programming language. However, many of them simply linearize the tree structure in order to input the AST into a neural network, which may cause a huge loss in the structural information. On the other hand, the recent hot topic graph neural network is capable of extracting structural information from graphs. My work proposed to apply graph neural network on AST to extract structural information from source code, thus detect code-clone. Though it’s a method designed for detecting cross-language code-clone, it’s currently under test stage on detecting same-language code-clone.

ABSTRACT. 分離論理における記号ヒープのための循環証明体系については，カット除去が不可能であることが知られている．しかし，ボトムアップに証明探索する場合，カット論理式を発見的に見つける必要があるカットの存在は問題となるため，発見的ではない手法でカット論理式を探索することができるようなカットの制限が期待される．そこで，このようなカットに対する制限のために，証明図のカットの下部に出現しうる論理式を推測可能と定義し，カット論理式を推測可能なものに制限することを考える．本発表では，記号ヒープのための循環証明体系においては，この制限されたカットによって証明能力が変わることを証明する．このことから，証明探索中に出現した論理式をカット論理式として利用するだけでは不十分であることが分かる．なお，本発表の内容は，FLOPS 2020 で発表予定である．

ABSTRACT. 本研究では，連続的な振舞い意味を持つ言語をサンプリングによる離散的な実行環境で実行するときに発生するエラーの検出を目的とする． Haskellのドメイン固有言語であるYampaはfunctional reactive programmingによってハイブリッドシステムを実現している． ここで，連続的な時間変化による連続値の変化はサンプリングによって実現されるため，重要なサンプリングポイントを逃すと連続的な振舞いは正しいプログラムであっても予期せぬエラーが発生する可能性がある． 我々は，Yampaプログラムが実現するハイブリッドシステムの振舞いを状態遷移システムでモデル化し，サンプリングを表現する時間オートマトンと並列実行することで，指定されたサンプリングのもとでYampaプログラムの振舞いをUppaalによって検証する手法を示す．

ABSTRACT. コードクローンとは、ソースコード中に現れる同一のコード断片または、類似したコード断片のことである。近年、コードクローン検出に関する研究が盛んに行われているが、関数型言語に特化したコードクローン検出手法は多くない。また関数型言語を対象として、構文は異なるが同じ意味を持つtype4のコードクローンを検出する手法に関する研究は、筆者らが調査した限り見当たらない。そこで本研究では、関数型言語Haskellを対象とし、type4のコードクローンを深層学習を用いて検出する。競技プログラミングサイトAtcoderから取得したソースコードを用いて実験した結果、83%の正解率でtype4のコードクローンが検出された。

ABSTRACT. 正規制約は制約プログラミングで利用されている制約の一種であり，ソフトウェアのモデル検査などに応用可能である． SATソルバーの性能は近年急速に向上しており，様々な分野においてSATを利用した問題解決手法が開発されている. 本研究では正規制約について，命題論理の充足可能性判定(SAT)問題に変換するSAT符号化方法を考案した． 性能を向上させるため，変換の際に違反点を範囲で表現し，2変数以下のみ含む制約の追加を行った． ベンチマークを設定し，既存ソルバーと比較を行った結果，既存ソルバーより性能が良いことを確認した.

ABSTRACT. Commit messages play an important role in comprehension of software evolution, as they represent records of code changes, such as feature additions and bug repairs. Unfortunately, developers sometimes are less motivated to follow coding standards, and neglect to write good commit messages due to the lack of direct benefits. In such scenarios, automatically generating commit messages can be a solution for this issue. Currently, there are two mainstream ways to generate commit messages, rule-based and learning-based. This poster will introduce the basic ideas behind current tools for commit messages generation, including rule-based tools and machine learning tools, and address some problems with state-of-the-art techniques. Moreover, the poster will propose some new ideas that haven’t been applied to this problem, and these ideas will be our future work to improve the current performance.

ABSTRACT. DNN CompilerをRustで実装している． 本発表では，量子化のエミュレーション時間短縮について述べる．

ABSTRACT. メソッドチェインスタイルでのプログラム記述は広く受け入れられていると言われている. しかし, そのことを示す定量的な結果は我々の知る限りでは存在しない. 本研究では「メソッドチェインスタイルが広く受け入れられているかどうか」を定量的に明らかにするため, メソッドチェインの出現数の経年変化を調査した. 分析の結果, ソースコード1行あたりの長さ2以上のメソッドチェインの出現数は2010年から2018年まで増加し続けていることが明らかになった. また, チェインされていないメソッド呼び出し数に対する, チェインされたメソッド呼び出し数の比率が2010年から2018年の間に16%から23%まで増加していることも明らかになった. さらに本発表では, 無作為抽出したメソッドチェインを人間が手作業で分類/分析して得られた結果と知見についても紹介する.

ABSTRACT. 短冊型問題とは、プログラミング作成問題の出題に適した問題形式であり、正解プログラムを行単位でばらばらにして不要な行を追加した上で並べ変え、選択記号をつけて選択肢とし、解答者は選択肢を並べて解答する。筆者らはこの方式を初年次プログラミング入門科目(800名)の期末試験に使用してきたが、学生は「endの不足」などの基本的な誤りを犯すことが多く見られる。そこで並べ替え後に「アドバイス」ボタンを押すと基本的な誤りを指摘するツールを作成し、使用は任意として公開した。その結果、ツールを使用した学生の方がそうでない学生より授業時間内の確認テストにおいて基本的な誤り数が少ないという結果が得られた。

ABSTRACT. Code completion recommends code fragments that the programmer likely to type in. One of the advanced code completion techniques is keyword programming, which can reflect the programmers’ intention. Keyword programming lets the user specify keywords and recommends expressions that contain as many of them. Another one is neural code completion, which uses neural networks to recommend likely occurring expressions according to the context (the program text preceding the cursor position). Previous work showed that the accuracy of a keyword programming system is not high enough. One of the reasons is that the existing keyword programming[1] always recommends shorter expressions without using the context information. In this paper, we improve keyword programming by combining a neural code completion technique. In addition to the occurrence of keyword, the ranking algorithm incorporates the likeliness factor of the code fragment concerning the context. To estimate the likeliness, we utilize a neural network-based sentence generator. Thus, we can achieve a more complicatedly suitable code fragment and generate a candidate list varying along with different contexts. We implemented our proposal for Java called ACKN as an Eclipse plug-in. The implementation is publicly available.