PPL 2020: 第22回プログラミングおよびプログラミング言語ワークショップ

This page contains an index consisting of author-provided keywords.

2
2flow	2flow, a composable computation graph-based computation model (ポスター・デモ)
A
Abstract Syntax Tree	Toward corss-language code-clone detection based on graph neural network (poster) Towards Generating Commit Messages Automatically (ポスター)
accounting	2flow, a composable computation graph-based computation model (ポスター・デモ)
Agda	[C1] Agda の Reflection API を用いた自動証明に向けて Agda による Equational Reasoning の証明の自動生成に向けて（ポスター） 関係代数及び関係データベースのAgdaによる定式化 Agda による対位法の定式化
Algebra	OCaml Blocklyを使用した代数教材の作成（ポスター・デモ）
Algebraic effect handlers	[C2] Handling Polymorphic Algebraic Effects
algebraic effects	[C1] algebraic effects を含むプログラムのステップ実行
B
backtracking	[C2] Functional Programming in Pattern-Match-Oriented Programming Style
behavioral metric	Codensity Games for Bisimilarity
bisimulation	Codensity Games for Bisimilarity
Brzozowski derivatives	先読み付き文脈自由文法とその微分
Brzozowski 微分	先読み付き文脈自由文法とその微分
Bytecode	Towards Generating Commit Messages Automatically (ポスター)
C
categorical gluing	計算効果と同変関手の圏論的貼り合わせ
categorical semantics	Toward a modalized linear-non-linear model
category theory	計算効果と同変関手の圏論的貼り合わせ
coalgebra	Codensity Games for Bisimilarity
Code Completion	ACKN: A context-aware keyword programming system (poster)
Code Generation	Quick and Reusable Code Generation for Idris
code-clone detection	Toward corss-language code-clone detection based on graph neural network (poster)
combinatorial testing	Toward combinatrial test generation using GPGPU
Commit Messages	Towards Generating Commit Messages Automatically (ポスター)
composability	2flow, a composable computation graph-based computation model (ポスター・デモ)
computation graph	2flow, a composable computation graph-based computation model (ポスター・デモ)
computation model	2flow, a composable computation graph-based computation model (ポスター・デモ)
computational effect	計算効果と同変関手の圏論的貼り合わせ
Computational effects	[C2] Handling Polymorphic Algebraic Effects
Context-free grammars	先読み付き文脈自由文法とその微分
Coq	[C1] Coq における Hylomorphism を用いたプログラム運算の検証に向けて [C1] Validating Mathematical Structures Coq における Hylomorphism を用いたプログラム運算の検証に向けて（ポスター） Formalized Egison − Egisonの型安全性のCoqによる証明に向けて(ポスター・デモ)
counterexample guided inductive synthesis	モデルの層化によるロバストなプログラム合成（ポスター・デモ）
CPS 変換	[C1] Agda の Reflection API を用いた自動証明に向けて
CPS変換	[C1] algebraic effects を含むプログラムのステップ実行
cross-language	Toward corss-language code-clone detection based on graph neural network (poster)
D
Dependent type theory	[C1] Validating Mathematical Structures
Dependently Typed Language	Quick and Reusable Code Generation for Idris
DNN Compiler	RustによるDNN Compilerの実装
Domain Specific Language	計算化学に向けたリファクタリング容易なドメイン特化言語のためのデザインの検討
Domain-specific language	[C2] Generating a Generic Fluent API in Java 2flow, a composable computation graph-based computation model (ポスター・デモ)
DSL	内部 DSL としての関数リアクティブプログラミング言語の実装手法（ポスター）
Dynamic object allocation	Sanajeh: a DSL for GPGPU programming with Python objects
E
Effectively Callback-Free Property	[C1] スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証
Egison	Formalized Egison − Egisonの型安全性のCoqによる証明に向けて(ポスター・デモ) パターンマッチ指向証明記述言語： Egisonパターンマッチをもちいた証明記述
Embedded Systems	FRPによるGPU上の計算の実現（ポスター）
Equational Reasoning	Agda による Equational Reasoning の証明の自動生成に向けて（ポスター）
extensible syntax	[C4] Wyvern: A Language for Usable Design-Driven Assurance
F
F*	[C1] F*を用いたMerkle Patricia Treeライブラリの形式検証
fault tolerance	[C2] HOPE: A Parallel Execution Model Based on Hierarchical Omission
FFI	Ruby から Javascript を呼び出す FFI における遠慮のかたまり問題について（ポスター・デモ）
fluent API	[C2] Generating a Generic Fluent API in Java [C2] Generating a Fluent API with Syntax Checking from an LR Grammar
Formalized mathematics	[C1] Validating Mathematical Structures
Functional Reactive Programming	FRPによるGPU上の計算の実現（ポスター）
G
GPGPU	Toward combinatrial test generation using GPGPU Sanajeh: a DSL for GPGPU programming with Python objects
GPU	FRPによるGPU上の計算の実現（ポスター）
GPU計算	Lift中間言語における動的長配列の追加(ポスター・デモ)
Graal (an alternative JIT compiler for HotSpot)	[C1] JITコンパイルにおけるコード配置効果の研究
graph neural network	Toward corss-language code-clone detection based on graph neural network (poster)
H
Haskell	Haskellを対象とした値コンストラクタへの関数注入によるトレース手法（ポスター・デモ） サンプリング時間実行におけるUppaalを用いたYampaプログラムの振舞い検証 関数型言語を対象としたtype4のコードクローンの検出手法の提案および実装（ポスター）
hidden class	Preforming Object Shapes for In-Object Field Allocation in eJS JavaScript VM (ポスター)
How to Design Programs	デザインレシピに沿ったプログラミング環境の実装
hylomorphism	[C1] Coq における Hylomorphism を用いたプログラム運算の検証に向けて Coq における Hylomorphism を用いたプログラム運算の検証に向けて（ポスター）
I
integrated development environments	[C2] An approach to generate text-based IDEs for syntax completion based on syntax specification
Intermediate Representation	Quick and Reusable Code Generation for Idris
J
Java	Object-oriented Programming with Versions
Java VM	[C1] JITコンパイルにおけるコード配置効果の研究
JavaScript	[C1] イベント駆動コードの差分解析を可能にするパス探査経験則 [C1] アプリケーションと実行環境に適応したカスタマイズ可能なJavaScript処理系 Preforming Object Shapes for In-Object Field Allocation in eJS JavaScript VM (ポスター)
JITコンパイラ	[C1] JITコンパイルにおけるコード配置効果の研究
Julia言語	Julia言語の型推論ルーチンを利用した型プロファイラによる静的なバグ検出について（ポスター・デモ）
just-in-time compiler	Making Different JIT Compilations Dancing to the Same Tune, Acting in the Meta-level
K
Keyword Programming	ACKN: A context-aware keyword programming system (poster)
L
language design	[C4] Wyvern: A Language for Usable Design-Driven Assurance Object-oriented Programming with Versions
language implementation	Making Different JIT Compilations Dancing to the Same Tune, Acting in the Meta-level
language systems	[C2] HOPE: A Parallel Execution Model Based on Hierarchical Omission
Let-polymorphism	[C2] Handling Polymorphic Algebraic Effects
library generation	[C2] Generating a Fluent API with Syntax Checking from an LR Grammar
Lift	Lift中間言語における動的長配列の追加(ポスター・デモ)
linear lambda-calculus	Toward a modalized linear-non-linear model
linear logic	Toward a modalized linear-non-linear model
Lisp	Homoiconic Lisp
LLVM IR	[C1] スタック領域上での時間的メモリ安全性を保証する静的解析手法 スタック領域上での時間的メモリ安全性を保証する静的解析手法の実装（デモ）
LNL model	Toward a modalized linear-non-linear model
logical predicate	計算効果と同変関手の圏論的貼り合わせ
Lookahead	先読み付き文脈自由文法とその微分
LR parsing	[C2] An approach to generate text-based IDEs for syntax completion based on syntax specification [C2] Generating a Fluent API with Syntax Checking from an LR Grammar
M
Machine Learning	Towards Generating Commit Messages Automatically (ポスター)
Macro	Homoiconic Lisp
memoization	[C2] Is Stateful Packrat Parsing Really Linear in Practice? -- A Counter-Example, an Improved Grammar, and Its Parsing Algorithms --
Merkle Patricia Tree	[C1] F*を用いたMerkle Patricia Treeライブラリの形式検証
Meta-programming	Homoiconic Lisp
meta-tracing JIT compiler	Making Different JIT Compilations Dancing to the Same Tune, Acting in the Meta-level
metaprogramming	[C2] Generating a Fluent API with Syntax Checking from an LR Grammar
modal logic	Toward a modalized linear-non-linear model
monoidal action	計算効果と同変関手の圏論的貼り合わせ
N
Neural Generation	ACKN: A context-aware keyword programming system (poster)
non-free data types	[C2] Functional Programming in Pattern-Match-Oriented Programming Style
non-linear pattern	[C2] Functional Programming in Pattern-Match-Oriented Programming Style
O
Object-oriented Language	Object-oriented Programming with Versions
OCaml	WebSocketを用いたUniverseフレームワークのブラウザ対応 OCaml Blockly のキー操作実装（ポスター）
OCaml Blockly	OCaml Blocklyを使用した代数教材の作成（ポスター・デモ） OCaml Blockly のキー操作実装（ポスター）
P
Packrat Parsing	[C2] Is Stateful Packrat Parsing Really Linear in Practice? -- A Counter-Example, an Improved Grammar, and Its Parsing Algorithms --
parallel execution model	[C2] HOPE: A Parallel Execution Model Based on Hierarchical Omission
Parallel programming	Sanajeh: a DSL for GPGPU programming with Python objects
Parallelization	FRPによるGPU上の計算の実現（ポスター）
Parametric polymorphism	[C2] Handling Polymorphic Algebraic Effects
Parsing expression grammars	[C2] Is Stateful Packrat Parsing Really Linear in Practice? -- A Counter-Example, an Improved Grammar, and Its Parsing Algorithms -- 先読み付き文脈自由文法とその微分
pattern-match-oriented programming	[C2] Functional Programming in Pattern-Match-Oriented Programming Style
PEG	Packrat ParserライブラリWoodrat用アルゴリズミックデバッガの実装
points-to解析	[C1] スタック領域上での時間的メモリ安全性を保証する静的解析手法 スタック領域上での時間的メモリ安全性を保証する静的解析手法の実装（デモ）
Processing	Processingプログラムにおけるイベント処理のユニットテスト手法（ポスター）
program synthesis	モデルの層化によるロバストなプログラム合成（ポスター・デモ）
Programming by Examples	[C1] 出力例を制約に用いたボトムアップなSQLクエリの合成
Proof assistants	[C1] Validating Mathematical Structures
Proof engineering	[C1] Validating Mathematical Structures
Python DSL	Sanajeh: a DSL for GPGPU programming with Python objects
Q
qubit connectivity	量子プログラムのための依存型を用いた coupling graph 解析（ポスター）
R
reactive programming	サンプリング時間実行におけるUppaalを用いたYampaプログラムの振舞い検証
reduction	[C2] An approach to generate text-based IDEs for syntax completion based on syntax specification
Reflection	[C1] Agda の Reflection API を用いた自動証明に向けて Agda による Equational Reasoning の証明の自動生成に向けて（ポスター）
Regular expressions	先読み付き文脈自由文法とその微分
RPython	Making Different JIT Compilations Dancing to the Same Tune, Acting in the Meta-level
Ruby	Ruby から Javascript を呼び出す FFI における遠慮のかたまり問題について（ポスター・デモ）
Rule-based Techniques	Towards Generating Commit Messages Automatically (ポスター)
runtime optimization	Preforming Object Shapes for In-Object Field Allocation in eJS JavaScript VM (ポスター)
Rust	[C2] RustHorn: CHC-based Verification for Rust Programs unsafe Rustプログラムの半自動正当性検証 内部 DSL としての関数リアクティブプログラミング言語の実装手法（ポスター） RustによるDNN Compilerの実装
S
safety game	Codensity Games for Bisimilarity
SAT符号化	正規制約に対するSAT符号化手法の提案と評価（ポスター）
SECD Machine	Homoiconic Lisp
secure languages	[C4] Wyvern: A Language for Usable Design-Driven Assurance
Selective CPS 変換	[C1] Agda の Reflection API を用いた自動証明に向けて
sentential forms	[C2] An approach to generate text-based IDEs for syntax completion based on syntax specification
SIMD命令	Wagon: 型安全性を持つSIMD命令を利用可能なDSL(ポスター・デモ)
SML#	[C1] 自然なデータ表現を持つ多相型言語のLLVM IRへのコンパイル方式
software architecture	[C4] Wyvern: A Language for Usable Design-Driven Assurance
software testing	Toward combinatrial test generation using GPGPU
Source code generation	[C2] Generating a Generic Fluent API in Java
SQL	[C1] 出力例を制約に用いたボトムアップなSQLクエリの合成 関係代数及び関係データベースのAgdaによる定式化
stateful parsing	[C2] Is Stateful Packrat Parsing Really Linear in Practice? -- A Counter-Example, an Improved Grammar, and Its Parsing Algorithms --
static analysis	Typing a Python Program by Unit Tests
stratified families of models	モデルの層化によるロバストなプログラム合成（ポスター・デモ）
stream fusion	より清浄なstream fusion（ポスター・デモ）
string-to-treeトランスデューサ	[C1] 正規表現マッチングの計算量解析ツールの拡張と高速化
syntax completion	[C2] An approach to generate text-based IDEs for syntax completion based on syntax specification
synthetic differential geometry	依存型付き微分λ計算 (ポスター)
Systems programming	unsafe Rustプログラムの半自動正当性検証
T
type inference	Typing a Python Program by Unit Tests
Type System	Object-oriented Programming with Versions
type4のコードクローン	関数型言語を対象としたtype4のコードクローンの検出手法の提案および実装（ポスター）
TypeScript	TypeScriptにおける型定義を切り替え可能な型検査補助ツールの実装（ポスター・デモ）
Typestate	Typestate 解析を応用した静的解析に よる 分散並行システムのバグの検出.
U
undo機能	OCaml Blockly のキー操作実装（ポスター）
unit test	Typing a Python Program by Unit Tests
Universeフレームワーク	WebSocketを用いたUniverseフレームワークのブラウザ対応
Uppaal	サンプリング時間実行におけるUppaalを用いたYampaプログラムの振舞い検証
V
V8	Ruby から Javascript を呼び出す FFI における遠慮のかたまり問題について（ポスター・デモ）
Verification	unsafe Rustプログラムの半自動正当性検証
visual programming language	2flow, a composable computation graph-based computation model (ポスター・デモ)
W
WebSocket	WebSocketを用いたUniverseフレームワークのブラウザ対応
Web実行環境	継続渡しスタイルの関数型プログラミング学習のためのWeb実行環境の実演（ポスター・デモ）
work omission	[C2] HOPE: A Parallel Execution Model Based on Hierarchical Omission
Y
Yampa	サンプリング時間実行におけるUppaalを用いたYampaプログラムの振舞い検証
Z
Z3	出力制約つき関数リアクティブシステムにおける入力センサの静的仕様推定(ポスター)
ν
νHFLZ	自動的なnu-HFLZ妥当性検査のための新しい篩型システム（ポスター・デモ）
ご
ごみ集め	[C1] アプリケーションと実行環境に適応したカスタマイズ可能なJavaScript処理系
ア
アノテーション	アサーションを取り入れた静的解析に基づくデバッグ支援ツール
アルゴリズミックデバッギング	Packrat ParserライブラリWoodrat用アルゴリズミックデバッガの実装
イ
イベント駆動コード	[C1] イベント駆動コードの差分解析を可能にするパス探査経験則
イベント駆動プログラミング	Processingプログラムにおけるイベント処理のユニットテスト手法（ポスター）
エ
エフェクトシステム	関数型プログラムの到達可能性検証のためのプログラムスライシング（ポスター）
エラーメッセージ	短冊型問題を用いたプログラミング学習用アドバイスツール(ポスター・デモ)
エンテイルメント判定問題	分離論理におけるエンテイルメント証明器の入力に対する制限の緩和(ポスター)
カ
カスタマイズ	[C1] アプリケーションと実行環境に適応したカスタマイズ可能なJavaScript処理系
カット規則	分離論理における記号ヒープのための循環証明体系におけるカットの制限について（ポスター）
カット除去(cut elimination)	入れ子対称λ計算の型規則　―上式が3つあるカットを持つ古典論理の証明体系―(ポスター)
ガ
ガベージコレクション	不揮発性メモリの性質に特化した書き込み回数を抑えるメモリ管理の提案(ポスター) Ruby から Javascript を呼び出す FFI における遠慮のかたまり問題について（ポスター・デモ）
キ
キー操作	OCaml Blockly のキー操作実装（ポスター）
ク
クオンテール	Preorders, partial semigroups, and quantales
グ
グラフ書き換え言語 LMNtal	グラフ書き換え言語 LMNtal による時間オートマトンに基づくリアルタイムシステムの状態空間構築 (ポスター)
グラフ書き換え言語LMNtal	階層グラフ書き換え言語LMNtalにおける継続の概念の提案と実装(ポスター) LMNtalにおける部分グラフのリサイクルを行うコンパイル時最適化（ポスター）
ゲ
ゲーム	OCaml Blocklyを使用した代数教材の作成（ポスター・デモ）
コ
コエフェクト計算	コエフェクト多相性に基づいた版多相性の実現
コンパイル時最適化	LMNtalにおける部分グラフのリサイクルを行うコンパイル時最適化（ポスター）
コードクローン	トークン列に対する曖昧検索技術の検討（ポスター）
コード生成	Lift中間言語における動的長配列の追加(ポスター・デモ)
コード生成系	Wagon: 型安全性を持つSIMD命令を利用可能なDSL(ポスター・デモ)
コード配置効果	[C1] JITコンパイルにおけるコード配置効果の研究
シ
シークエント計算	不動点算術の循環証明体系 (ポスター)
ス
スタックフレーム	[C1] スタック領域上での時間的メモリ安全性を保証する静的解析手法 スタック領域上での時間的メモリ安全性を保証する静的解析手法の実装（デモ）
スタック木変換器	スタック機構を搭載する木変換器（ポスター）
ステッパ	[C1] algebraic effects を含むプログラムのステップ実行
ステートレスモデル検査	弱いメモリモデル上での並行Cライブラリのステートレスモデル検査
ストリーム	より清浄なstream fusion（ポスター・デモ）
スマートコントラクト	[C1] スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証 ReFX: 型に基づくスマートコントラクト自動検証器（ポスター・デモ）
タ
タスク並列言語	並列言語Tascellのタスク定義自動生成による記述性向上（ポスター）
デ
デザインレシピ	デザインレシピに沿ったプログラミング環境の実装
デバッガ	アサーションを取り入れた静的解析に基づくデバッグ支援ツール
デバッグ	Packrat ParserライブラリWoodrat用アルゴリズミックデバッガの実装
データフロー解析	[C1] スタック領域上での時間的メモリ安全性を保証する静的解析手法 スタック領域上での時間的メモリ安全性を保証する静的解析手法の実装（デモ）
データベース	関係代数及び関係データベースのAgdaによる定式化
ト
トレース手法	Haskellを対象とした値コンストラクタへの関数注入によるトレース手法（ポスター・デモ）
ド
ドメイン特化言語	型ディスパッチコード最適化のためのJavaScript処理系記述用DSLの型推論（ポスター）
ニ
ニューラルネットワーク	関数型言語を対象としたtype4のコードクローンの検出手法の提案および実装（ポスター）
ハ
ハイブリッドシステム	サンプリング時間実行におけるUppaalを用いたYampaプログラムの振舞い検証
パ
パターンマッチ	Formalized Egison − Egisonの型安全性のCoqによる証明に向けて(ポスター・デモ) パターンマッチ指向証明記述言語： Egisonパターンマッチをもちいた証明記述
パッケージマネージャ	パッケージマネージャにおけるパッケージの依存関係の事前計算によるパッケージ取得時間の短縮（ポスター・デモ）
ビ
ビジュアルプログラミング環境	OCaml Blocklyを使用した代数教材の作成（ポスター・デモ）
フ
フラット項書き換えシステム	フラット項書き換えシステムの簡約に関する一意正規形性の決定不能性(ポスター)
ブ
ブロックプログラミング	OCaml Blocklyを使用した代数教材の作成（ポスター・デモ）
ブロックプログラミング環境	OCaml Blockly のキー操作実装（ポスター）
プ
プログラマビリティ	並列言語Tascellのタスク定義自動生成による記述性向上（ポスター）
プログラミング学習	継続渡しスタイルの関数型プログラミング学習のためのWeb実行環境の実演（ポスター・デモ）
プログラミング教育	[C1] Puppy: 高校生向けの簡易 Python の設計と実装 短冊型問題を用いたプログラミング学習用アドバイスツール(ポスター・デモ)
プログラミング環境	デザインレシピに沿ったプログラミング環境の実装
プログラミング補助ツール	TypeScriptにおける型定義を切り替え可能な型検査補助ツールの実装（ポスター・デモ）
プログラムスライシング	関数型プログラムの到達可能性検証のためのプログラムスライシング（ポスター）
プログラム可視化	[C1] Puppy: 高校生向けの簡易 Python の設計と実装
プログラム合成	[C1] 出力例を制約に用いたボトムアップなSQLクエリの合成
プログラム検証	篩型と所有権を用いたプログラム検証に対する反例生成 (ポスター‧デモ) 自動的なnu-HFLZ妥当性検査のための新しい篩型システム（ポスター・デモ） ReFX: 型に基づくスマートコントラクト自動検証器（ポスター・デモ）
プログラム解析	分離論理を用いた再帰プログラムのメモリ安全性検査
プログラム運算	[C1] Coq における Hylomorphism を用いたプログラム運算の検証に向けて Coq における Hylomorphism を用いたプログラム運算の検証に向けて（ポスター）
ベ
ベクトル化	Wagon: 型安全性を持つSIMD命令を利用可能なDSL(ポスター・デモ)
マ
マクロプログラミング	WSAN向けマクロプログラミング言語の提案（ポスター）
マルチステージプログラミング	依存型を備えた多段階計算の同値型による拡張(ポスター)
マルチスレッド	パッケージマネージャにおけるパッケージの依存関係の事前計算によるパッケージ取得時間の短縮（ポスター・デモ）
メ
メソッドチェイン	メソッドチェイン形式の記述に関する調査（ポスター）
メタプログラミング	[C1] Agda の Reflection API を用いた自動証明に向けて より清浄なstream fusion（ポスター・デモ）
メモリモデル	弱いメモリモデル上での並行Cライブラリのステートレスモデル検査
メモリ安全性	[C1] スタック領域上での時間的メモリ安全性を保証する静的解析手法 分離論理を用いた再帰プログラムのメモリ安全性検査 スタック領域上での時間的メモリ安全性を保証する静的解析手法の実装（デモ）
メモリ管理	不揮発性メモリの性質に特化した書き込み回数を抑えるメモリ管理の提案(ポスター)
モ
モジュールシステム	コエフェクト多相性に基づいた版多相性の実現
ユ
ユニットテスト	Processingプログラムにおけるイベント処理のユニットテスト手法（ポスター）
ラ
ラムダ計算	継続渡しスタイルの関数型プログラミング学習のためのWeb実行環境の実演（ポスター・デモ）
リ
リアルタイムシステム	グラフ書き換え言語 LMNtal による時間オートマトンに基づくリアルタイムシステムの状態空間構築 (ポスター)
レ
レポジトリマイニング	メソッドチェイン形式の記述に関する調査（ポスター）
不
不動点算術	不動点算術の循環証明体系 (ポスター)
不揮発性メモリ	不揮発性メモリの性質に特化した書き込み回数を抑えるメモリ管理の提案(ポスター)
並
並列計算	計算化学に向けたリファクタリング容易なドメイン特化言語のためのデザインの検討
並行ライブラリ	弱いメモリモデル上での並行Cライブラリのステートレスモデル検査
事
事前計算	パッケージマネージャにおけるパッケージの依存関係の事前計算によるパッケージ取得時間の短縮（ポスター・デモ）
交
交叉手法	遺伝的アルゴリズムを用いた最短経路探索における交叉手法開発（ポスター）
交換律	[C1] 交換律による正則項書き換えにおける有限オートマトンの構成法とその応用
仮
仮想機械	[C1] アプリケーションと実行環境に適応したカスタマイズ可能なJavaScript処理系 型ディスパッチコード最適化のためのJavaScript処理系記述用DSLの型推論（ポスター）
余
余帰納的定理	等式論理の余帰納的定理における圏論の応用(ポスター)
依
依存型	依存型付き微分λ計算 (ポスター) Agda による対位法の定式化 量子プログラムのための依存型を用いた coupling graph 解析（ポスター） 依存型を備えた多段階計算の同値型による拡張(ポスター)
依存関係	パッケージマネージャにおけるパッケージの依存関係の事前計算によるパッケージ取得時間の短縮（ポスター・デモ）
充
充足可能性判定	正規制約に対するSAT符号化手法の提案と評価（ポスター） 解集合ソルバーを用いた様相命題論理の充足可能性判定 (ポスター)
先
先読み	先読み付き文脈自由文法とその微分
内
内部データ表現	[C1] アプリケーションと実行環境に適応したカスタマイズ可能なJavaScript処理系
分
分散システム	WSAN向けマクロプログラミング言語の提案（ポスター）
分散並行システム	Typestate 解析を応用した静的解析に よる 分散並行システムのバグの検出.
分離論理	分離論理を用いた再帰プログラムのメモリ安全性検査 分離論理における記号ヒープのための循環証明体系におけるカットの制限について（ポスター） 分離論理におけるエンテイルメント証明器の入力に対する制限の緩和(ポスター)
到
到達可能性解析	関数型プログラムの到達可能性検証のためのプログラムスライシング（ポスター）
動
動的負荷分散	並列言語Tascellのタスク定義自動生成による記述性向上（ポスター）
十
十分完全性	[C1] 項書き換えシステムにおける局所十分完全性の証明法
双
双対性	等式論理の余帰納的定理における圏論の応用(ポスター)
双方向変換	トレースに基づく双方向変換の多方向化に向けたco-targetial compositionのための漸進化（ポスター）
反
反例	篩型と所有権を用いたプログラム検証に対する反例生成 (ポスター‧デモ)
古
古典論理(classical logic)	入れ子対称λ計算の型規則　―上式が3つあるカットを持つ古典論理の証明体系―(ポスター)
合
合成	トレースに基づく双方向変換の多方向化に向けたco-targetial compositionのための漸進化（ポスター）
合流性	[C1] 条件付き項書き換えシステムの階層合流性証明法
同
同値型	依存型を備えた多段階計算の同値型による拡張(ポスター)
圏
圏論	等式論理の余帰納的定理における圏論の応用(ポスター) 依存型付き微分λ計算 (ポスター)
型
型システム	[C1] 小規模組込みシステム向けFRP言語に対する再帰的データ型の導入 [C1] スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証 [C2] RustHorn: CHC-based Verification for Rust Programs Formalized Egison − Egisonの型安全性のCoqによる証明に向けて(ポスター・デモ) コエフェクト多相性に基づいた版多相性の実現
型主導コンパイル	[C1] 自然なデータ表現を持つ多相型言語のLLVM IRへのコンパイル方式
型安全性	Wagon: 型安全性を持つSIMD命令を利用可能なDSL(ポスター・デモ)
型定義ファイル	TypeScriptにおける型定義を切り替え可能な型検査補助ツールの実装（ポスター・デモ）
型推論	Julia言語の型推論ルーチンを利用した型プロファイラによる静的なバグ検出について（ポスター・デモ）
型検査器	TypeScriptにおける型定義を切り替え可能な型検査補助ツールの実装（ポスター・デモ）
型理論	Lift中間言語における動的長配列の追加(ポスター・デモ) 依存型を備えた多段階計算の同値型による拡張(ポスター)
型解析	型ディスパッチコード最適化のためのJavaScript処理系記述用DSLの型推論（ポスター）
多
多方向変換	トレースに基づく双方向変換の多方向化に向けたco-targetial compositionのための漸進化（ポスター）
多段階計算	より清浄なstream fusion（ポスター・デモ）
存
存在型	Lift中間言語における動的長配列の追加(ポスター・デモ)
学
学習評価	短冊型問題を用いたプログラミング学習用アドバイスツール(ポスター・デモ)
定
定理証明システム	パターンマッチ指向証明記述言語： Egisonパターンマッチをもちいた証明記述
定理証明支援系言語	[C1] Agda の Reflection API を用いた自動証明に向けて
定量的分析	メソッドチェイン形式の記述に関する調査（ポスター）
対
対位法	Agda による対位法の定式化
対称λ計算(symmetric lambda calculus)	入れ子対称λ計算の型規則　―上式が3つあるカットを持つ古典論理の証明体系―(ポスター)
局
局所十分完全性	[C1] 項書き換えシステムにおける局所十分完全性の証明法
差
差分解析	[C1] イベント駆動コードの差分解析を可能にするパス探査経験則
帰
帰納的定理	等式論理の余帰納的定理における圏論の応用(ポスター)
帰納的述語	分離論理におけるエンテイルメント証明器の入力に対する制限の緩和(ポスター)
強
強正規化性	[C1] 古典論理に対する汎用的自然演繹の証明正規化
形
形式検証	[C1] F*を用いたMerkle Patricia Treeライブラリの形式検証
循
循環参照	Ruby から Javascript を呼び出す FFI における遠慮のかたまり問題について（ポスター・デモ）
循環証明体系	分離論理における記号ヒープのための循環証明体系におけるカットの制限について（ポスター） 不動点算術の循環証明体系 (ポスター)
微
微分λ計算	依存型付き微分λ計算 (ポスター)
性
性能評価	[C1] JITコンパイルにおけるコード配置効果の研究
所
所有権	[C2] RustHorn: CHC-based Verification for Rust Programs 篩型と所有権を用いたプログラム検証に対する反例生成 (ポスター‧デモ)
抽
抽象解釈	Julia言語の型推論ルーチンを利用した型プロファイラによる静的なバグ検出について（ポスター・デモ）
探
探査経験則	[C1] イベント駆動コードの差分解析を可能にするパス探査経験則
推
推測可能	分離論理における記号ヒープのための循環証明体系におけるカットの制限について（ポスター）
教
教材	OCaml Blocklyを使用した代数教材の作成（ポスター・デモ）
教育言語	[C1] Puppy: 高校生向けの簡易 Python の設計と実装
文
文脈自由文法	先読み付き文脈自由文法とその微分
時
時間オートマトン	グラフ書き換え言語 LMNtal による時間オートマトンに基づくリアルタイムシステムの状態空間構築 (ポスター)
暗
暗号通貨	ReFX: 型に基づくスマートコントラクト自動検証器（ポスター・デモ）
曖
曖昧検索	トークン列に対する曖昧検索技術の検討（ポスター）
最
最短経路問題	遺伝的アルゴリズムを用いた最短経路探索における交叉手法開発（ポスター）
最適化	より清浄なstream fusion（ポスター・デモ）
有
有限オートマトン	[C1] 交換律による正則項書き換えにおける有限オートマトンの構成法とその応用
木
木変換器	スタック機構を搭載する木変換器（ポスター）
条
条件付き項書き換えシステム	[C1] 条件付き項書き換えシステムの階層合流性証明法
構
構文解析器	スタック機構を搭載する木変換器（ポスター）
様
様相命題論理	解集合ソルバーを用いた様相命題論理の充足可能性判定 (ポスター)
機
機械学習	RustによるDNN Compilerの実装
正
正則項	[C1] 交換律による正則項書き換えにおける有限オートマトンの構成法とその応用
正則項書き換え	[C1] 交換律による正則項書き換えにおける有限オートマトンの構成法とその応用
正規制約	正規制約に対するSAT符号化手法の提案と評価（ポスター）
正規表現	先読み付き文脈自由文法とその微分
正規表現マッチング	[C1] 正規表現マッチングの計算量解析ツールの拡張と高速化
決
決定不能性	フラット項書き換えシステムの簡約に関する一意正規形性の決定不能性(ポスター)
深
深層学習	関数型言語を対象としたtype4のコードクローンの検出手法の提案および実装（ポスター）
漸
漸進化	トレースに基づく双方向変換の多方向化に向けたco-targetial compositionのための漸進化（ポスター）
無
無線センサーアクターネットワーク	WSAN向けマクロプログラミング言語の提案（ポスター）
状
状態遷移	状態遷移を表現する組込みシステム向けFRP言語の設計（ポスター）
短
短冊型問題	短冊型問題を用いたプログラミング学習用アドバイスツール(ポスター・デモ)
科
科学技術計算	計算化学に向けたリファクタリング容易なドメイン特化言語のためのデザインの検討
等
等式論理	等式論理の余帰納的定理における圏論の応用(ポスター)
篩
篩型	篩型と所有権を用いたプログラム検証に対する反例生成 (ポスター‧デモ) ReFX: 型に基づくスマートコントラクト自動検証器（ポスター・デモ）
篩型システム	自動的なnu-HFLZ妥当性検査のための新しい篩型システム（ポスター・デモ）
簡
簡約に関する一意正規形	フラット項書き換えシステムの簡約に関する一意正規形性の決定不能性(ポスター)
組
組み込みシステム	WSAN向けマクロプログラミング言語の提案（ポスター）
組み込み開発	内部 DSL としての関数リアクティブプログラミング言語の実装手法（ポスター）
組込みシステム	[C1] 小規模組込みシステム向けFRP言語に対する再帰的データ型の導入 出力制約つき関数リアクティブシステムにおける入力センサの静的仕様推定(ポスター) 状態遷移を表現する組込みシステム向けFRP言語の設計（ポスター）
継
継続	階層グラフ書き換え言語LMNtalにおける継続の概念の提案と実装(ポスター)
継続(continuation)	入れ子対称λ計算の型規則　―上式が3つあるカットを持つ古典論理の証明体系―(ポスター)
継続渡しスタイル	継続渡しスタイルの関数型プログラミング学習のためのWeb実行環境の実演（ポスター・デモ）
自
自動検証	[C2] RustHorn: CHC-based Verification for Rust Programs
自動証明	[C1] Agda の Reflection API を用いた自動証明に向けて Agda による Equational Reasoning の証明の自動生成に向けて（ポスター） 分離論理におけるエンテイルメント証明器の入力に対する制限の緩和(ポスター)
自然演繹	[C1] 古典論理に対する汎用的自然演繹の証明正規化
解
解析表現文法	先読み付き文脈自由文法とその微分
解集合プログラミング	解集合ソルバーを用いた様相命題論理の充足可能性判定 (ポスター)
言
言語処理系	Haskellを対象とした値コンストラクタへの関数注入によるトレース手法（ポスター・デモ）
言語設計	[C1] Puppy: 高校生向けの簡易 Python の設計と実装
計
計算量解析	[C1] 正規表現マッチングの計算量解析ツールの拡張と高速化
記
記号ヒープ	分離論理における記号ヒープのための循環証明体系におけるカットの制限について（ポスター）
記号実行	[C1] イベント駆動コードの差分解析を可能にするパス探査経験則
証
証明探索	分離論理における記号ヒープのための循環証明体系におけるカットの制限について（ポスター）
証明正規化	[C1] 古典論理に対する汎用的自然演繹の証明正規化
誤
誤りの指摘	短冊型問題を用いたプログラミング学習用アドバイスツール(ポスター・デモ)
遺
遺伝的アルゴリズム	遺伝的アルゴリズムを用いた最短経路探索における交叉手法開発（ポスター）
部
部分グラフ再利用	LMNtalにおける部分グラフのリサイクルを行うコンパイル時最適化（ポスター）
部分型付け	自動的なnu-HFLZ妥当性検査のための新しい篩型システム（ポスター・デモ）
部分論理式性	[C1] 古典論理に対する汎用的自然演繹の証明正規化
量
量子ラムダ計算	量子プログラムのための依存型を用いた coupling graph 解析（ポスター）
関
関係代数	関係代数及び関係データベースのAgdaによる定式化
関係埋め込み	Preorders, partial semigroups, and quantales
関手	Preorders, partial semigroups, and quantales
関数リアクティブプログラミング	[C1] 小規模組込みシステム向けFRP言語に対する再帰的データ型の導入 出力制約つき関数リアクティブシステムにおける入力センサの静的仕様推定(ポスター) 内部 DSL としての関数リアクティブプログラミング言語の実装手法（ポスター） 状態遷移を表現する組込みシステム向けFRP言語の設計（ポスター）
関数型プログラミング	Wagon: 型安全性を持つSIMD命令を利用可能なDSL(ポスター・デモ) 継続渡しスタイルの関数型プログラミング学習のためのWeb実行環境の実演（ポスター・デモ）
関数型プログラミング言語	Haskellを対象とした値コンストラクタへの関数注入によるトレース手法（ポスター・デモ） 関係代数及び関係データベースのAgdaによる定式化
関数型言語	[C1] 自然なデータ表現を持つ多相型言語のLLVM IRへのコンパイル方式 関数型言語を対象としたtype4のコードクローンの検出手法の提案および実装（ポスター）
限
限定継続	[C1] algebraic effects を含むプログラムのステップ実行 階層グラフ書き換え言語LMNtalにおける継続の概念の提案と実装(ポスター)
階
階層合流性	[C1] 条件付き項書き換えシステムの階層合流性証明法
静
静的検査	トークン列に対する曖昧検索技術の検討（ポスター）
静的検証	[C1] スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証
静的解析	[C1] スタック領域上での時間的メモリ安全性を保証する静的解析手法 Julia言語の型推論ルーチンを利用した型プロファイラによる静的なバグ検出について（ポスター・デモ） スタック領域上での時間的メモリ安全性を保証する静的解析手法の実装（デモ） Typestate 解析を応用した静的解析に よる 分散並行システムのバグの検出. アサーションを取り入れた静的解析に基づくデバッグ支援ツール
非
非決定的バグ	Typestate 解析を応用した静的解析に よる 分散並行システムのバグの検出.
非関数化	[C1] algebraic effects を含むプログラムのステップ実行
項
項書き換えシステム	[C1] 条件付き項書き換えシステムの階層合流性証明法 [C1] 項書き換えシステムにおける局所十分完全性の証明法
高
高階不動点算術	不動点算術の循環証明体系 (ポスター)
高階関数型	自動的なnu-HFLZ妥当性検査のための新しい篩型システム（ポスター・デモ）

Disclaimer | Powered by EasyChair Smart Program