所属
大学院情報学研究科 情報システム学専攻 計算論 教授
大学院担当
大学院情報学研究科
学部担当
工学部
情報学部 コンピュータ科学科
情報学部 コンピュータ科学科
職名
教授
サカイ マサヒコ
酒井 正彦
SAKAI, Masahiko
現在の研究課題とSDGs
現在の研究課題とSDGs 4
-
SQLに基づく組み合わせ問題記述法とそのソルバ
-
Midiからの自動採譜
-
項書換え系の基礎研究
-
擬ブール制約問題ソルバ
学歴
学歴 3
-
名古屋大学 工学研究科 電気工学,電気工学第二及び電子工学専攻
1986年4月 - 1989年3月
詳細を見る
国名： 日本国
-
名古屋大学 工学研究科 電気工学,電気工学第二及び電子工学専攻
1984年4月 - 1986年3月
詳細を見る
国名： 日本国
-
名古屋大学 工学部 電気学科
1980年4月 - 1984年3月
詳細を見る
国名： 日本国
委員歴
委員歴 26
-
9th International workshop on rewriting techniques for program transformations and evaluation (WPTE 2022) Program committee member
2022年1月 - 2022年7月
-
7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022) Program Committee Member
2021年3月 - 2022年11月
-
7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022) Program Committee Member
2021年3月 - 2022年11月
-
30th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2020) Program Committee Member
2020年1月 - 2020年11月
-
4th International workshop on rewriting techniques for program transformations and evaluation (WPTE 2017) Program committee member
2017年1月 - 2017年7月
-
8th International Joint Conference on Automated Reasoning (IJCAR 2016) Program Committee Member
2015年12月 - 2016年7月
-
2nd International workshop on rewriting techniques for program transformations and evaluation (WPTE 2015) Program committee member
2015年1月 - 2015年7月
-
26th International Conference on Rewriting Techniques and Applications (RTA 2015) Program Committee Member
2014年10月 - 2015年7月
-
1st International workshop on rewriting techniques for program transformations and evaluation (WPTE 2014) Program committee co-Chair
2014年1月 - 2014年7月
-
23rd International Conference on Rewriting Techniques and Applications (RTA 2012) General Chair and Program Committee Member
2012年5月 - 2012年6月
-
10th International workshop on reduction strategies in rewriting and programming (WRS 2007) Program committee member
2010年7月
-
International Conference on Rewriting Techniques and Applications (RTA) Steering Committee member
2010年6月 - 2013年5月
-
International Conference on Rewriting Techniques and Applications (RTA) Publicity Chair
2010年6月 - 2011年5月
-
電子情報通信学会 ソフトウェアサイエンス研究専門委員会 専門委員
2010年5月 - 現在
-
8th International workshop on reduction strategies in rewriting and programming (WRS 2007) Program committee member
2008年7月
-
電子情報通信学会 フォーマルアプローチ特集号 編集委員会 委員
2008年5月 - 2009年4月
-
7th International workshop on reduction strategies in rewriting and programming (WRS 2007) Program committee member
2007年6月
-
電子情報通信学会 フォーマルアプローチ特集号 編集委員会 委員長
2007年5月 - 2008年4月
-
電子情報通信学会 フォーマルアプローチ特集号 編集委員会 副委員長
2006年5月 - 2007年4月
-
第8回プログラミングおよびプログラミング言語ワークショップ(PPL2006) プログラム委員会 委員
2006年3月
-
電子情報通信学会 フォーマルアプローチ特集号 編集委員会 委員
2005年5月 - 2006年4月
-
電子情報通信学会 英文論文誌 理論計算機科学特集号 編集委員会 委員
2005年2月 - 現在
-
第19回 日本ソフトウェア科学会大会 プログラム委員 委員
2002年9月
-
第18回 日本ソフトウェア科学会大会 プログラム委員 委員
2001年9月
-
電子情報通信学会 コンピュテーション研究専門委員会 専門委員
1999年4月 - 2005年3月
-
電子情報通信学会 ソフトウェアサイエンス研究専門委員会 幹事
1992年4月 - 1996年3月
受賞
受賞 3
-
第67回 平成22年度 電子情報通信学会論文賞
2011年5月 電子情報通信学会
詳細を見る
受賞国：日本国
-
第48回 平成3年度 電子情報通信学会論文賞
1992年5月 電子情報通信学会
詳細を見る
受賞国：日本国
-
Winner in the Inspiring Idea Track on International Competition on Graph Counting Algorithms
2023年9月
Kosuke Oguri, Kenji Hashimoto, and Masahiko Sakai
論文
論文 218
-
拍対応情報の利用による楽譜と実演奏の音符対応情報の自動生成法
佐藤 宏志, 酒井 正彦
情報処理学会技術報告 SIGMUS 142 巻 2025年3月
詳細を見る
担当区分：最終著者, 責任著者 記述言語：日本語 掲載種別：研究論文（研究会，シンポジウム資料等）
-
Solving Rep-Tile by Computers: Performance of Solvers and Analyses of Solutions 招待有り
Mutsunori Banbara, Kenji Hashimoto, Takashi Horiyama, Kosuke Oguri, Shin-ichi Minato, Masaaki Nishino, Masahiko Sakai, Ryuhei Uehara, Yushi Uno, and Norihito Yasuda
Algorithmic Foundations for Social Advancement 頁： 187 - 208 2025年3月
詳細を見る
-
Tokenization of MIDI Sequences for Transcription 査読有り 国際共著
Florent Jacquemard, Masahiko Sakai, Yosuke Amagasu
Proceedings of the International Conference on Technologies for Music Notation and Representation (TENOR 2024) 頁： 98 - 108 2024年4月
詳細を見る
-
演奏MIDIのリズム量子化のためのトークン化の提案
天春 陽介, 酒井 正彦
情報処理学会技術報告 SIGMUS 2024年3月
詳細を見る
担当区分：最終著者, 責任著者 記述言語：日本語 掲載種別：研究論文（研究会，シンポジウム資料等）
-
8+8=4: Formalizing Time Units to Handle Symbolic Music Durations 査読有り 国際共著
Emmanouil Karystinaios, Francesco Foscarin, Florent Jacquemard, Masahiko Sakai, Satoshi Tojo and Gerhard Widmer
The 16th International Symposium on Computer Music Multidisciplinary Research 頁： 536 - 546 2023年9月
詳細を見る
-
Automatic Phrasing System for Expressive Performance Based on The Generative Theory of Tonal Music 査読有り
Madoka Goto, Masahiko Sakai, Satoshi Tojo
The 16th International Symposium on Computer Music Multidisciplinary Research 頁： 536 - 546 2023年9月
詳細を見る
-
Ground Canonical Rewrite Systems Revisited 査読有り 国際共著
Aart Middeldorp, Masahiko Sakai, Sarah Winkler
12th International Workshop on Confluence 頁： 44 - 48 2023年8月
詳細を見る
担当区分：責任著者 記述言語：英語 掲載種別：研究論文（国際会議プロシーディングス）
-
SQL 型制約プログラミングシステム CombSQL+ の複数制約ソルバー連携
小菅 脩司、酒井 正彦、番原 睦則
人工知能学会研究会資料 125 巻 頁： 54 - 59 2023年8月
詳細を見る
-
レプ・タイルの定式化を用いた各種ソルバの性能比較
番原 睦則, 橋本 健二, 堀山 貴史, 湊 真一, 中村 駆, 西野 正彬, 酒井 正彦, 上原 隆平, 宇野 裕之, 安田 宜仁
人工知能学会研究会資料 人工知能基本問題研究会 119 巻 ( 0 ) 頁： 02 - 07 2022年1月
詳細を見る
-
Solving Rep-tile by Computers: Performance of Solvers and Analyses of Solutions
Mutsunori Banbara, Kenji Hashimoto, Takashi Horiyama, Shin-ichi Minato, Kakeru Nakamura, Masaaki Nishino, Masahiko Sakai, Ryuhei Uehara, Yushi Uno, Norihito Yasuda
arXiv 2110.05184 2021年10月
詳細を見る
-
SQL 型ソルバ CombSQL+による車両割当て問題の記述
井上 和哉, 岸 潤一郎, 酒井 正彦
人工知能学会全国大会論文集 JSAI2021 巻 ( 0 ) 頁： 2E4OS13c01 - 2E4OS13c01 2021年6月
詳細を見る
担当区分：最終著者, 責任著者 記述言語：日本語 掲載種別：研究論文（研究会，シンポジウム資料等） 出版者・発行元：一般社団法人 人工知能学会
<p>著者らはこれまで，SQL 言語を知っていれば組合せ最適化問題を比較的容易に記述し解くことができるようにすることを目的として，CombSQL+システムを開発した．まだこのシステムの利用例は少なく，応用例を増やし評価することが必要である. 本稿では，車両割当て問題に対するCombSQL+の記述を紹介する．ここで，些細とも思われる記述の差が，大きく実行性能に影響を及ぼす事が分かった．その理由について考察し，解決法のアイデアを述べる．</p>
-
Transformation of SQL-based Combinatorial Optimization Problems into Constraint Problems
Genki Sakanashi, Masahiko Sakai
SIG-FPAI-112 112 巻 ( 4 ) 頁： 6pages 2020年3月
詳細を見る
記述言語：英語
-
Conditions for Confluence of Innermost Terminating Term Rewriting Systems 査読有り
Sayaka Ishizuki, Masahiko Sakai, and Michio Oyamaguchi
Applicable Algebra in Engineering, Communication and Computing 30 巻 ( 4 ) 頁： 349-360 2019年8月
詳細を見る
-
A Parse-based Framework for Coupled Rhythm Quantization and Score Structuring 査読有り
Francesco Foscarin, Florent Jacquemard, Philippe Rigaux, and Masahido Sakai
Lecture Notes in Artificial Intelligence 11502 巻 頁： 248-260 2019年6月
詳細を見る
-
Transformation of Combinatorial Optimization Problems Written in Extended SQL into Constraint Problems 査読有り
Genki Sakanashi and Masahiko Sakai
Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming (PPDP 2018) 頁： 19:1-19:13 2018年9月
詳細を見る
-
Reduced dependency spaces for existential parameterised Boolean equation system 査読有り
Yutaro Nagae, Masahiko Sakai
Electronic Proceedins in Theoretical Computer Science (EPTCS) 265 巻 頁： 67-81 2018年1月
詳細を見る
-
Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers 査読有り
Tomohiro Sasano, Naoki Nishida, Masahiko Sakai, and Tomoya Ueyama
Electronic Proceedins in Theoretical Computer Science (EPTCS) 265 巻 頁： 82-97 2018年1月
詳細を見る
-
Generating Equivalent Rhythmic Notations Based on Rhythm Tree Languages 査読有り
Florent Jacquemard, Adrien Ycart, and Masahiko Sakai
Proceedings of the International Conference on Technologies for Music Notation and Representation 頁： 145-153 2017年5月
詳細を見る
記述言語：英語
-
Sound Structure-Preserving Transformation for Weakly-Left-Linear Deterministic Conditional Term Rewriting Systems 査読有り
Ryota Nakayama, Naoki Nishida and Masahiko Sakai
Electronic Proceedins in Theoretical Computer Science 235 巻 頁： 62-77 2017年1月
詳細を見る
-
An extension of proof graphs for disjunctive parameterised Boolean equation systems 査読有り
Yutaro Nagae, and Masahiko Sakai and Hiroyuki Seki
Electronic Proceedins in Theoretical Computer Science 235 巻 頁： 46-61 2017年1月
詳細を見る
-
An extension of proof graphs for disjunctive parameterised Boolean equation systems 査読有り
Yutaro Nagae, Masahiko Sakai
Informal Proceedings of the 3rd International Workshop on Rewriting Techniques f or Program Transformations and Evaluation (WPTE 2016) 頁： 3-14 2016年9月
詳細を見る
記述言語：英語
-
Sound Structure-Preserving Transformation for Ultra-Weakly-Left-Linear Determini stic Conditional Term Rewriting Systems 査読有り
Ryota Nakayama, Naoki Nishida, Masahiko Sakai
Informal Proceedings of the 3rd International Workshop on Rewriting Techniques f or Program Transformations and Evaluation (WPTE 2016) 頁： 61-75 2016年9月
詳細を見る
記述言語：英語
-
Conditions for confluence of innermost terminating term rewriting systems 査読有り
Sayaka Ishizuki, Masahiko Sakai, Michio Oyamaguchi
Proceedings of the 5th International Workshop on Confluence (IWC 2016) 頁： 65-69 2016年9月
詳細を見る
記述言語：英語
-
Term Rewriting with Prefix Context Constraints and Regularity Preservation and Bottom-Up Strategies 査読有り
Yoshiharu Kojima, Masahiko Sakai, Florent Jacquemard
Lecture Notes in Computer Science (CADE 2015) 9195 巻 頁： 137-151 2015年8月
詳細を見る
記述言語：英語
-
Non-E-overlapping, weakly shallow, and non-collapsing TRSs are confluent 査読有り
Masahiko Sakai, Michio Oyamaguchi, Mizuhito Ogawa
Lecture Notes in Computer Science (CADE 2015) 9195 巻 頁： 111-126 2015年8月
詳細を見る
-
Construction of an ROBDD for a PB-constraint in band form and related techniques for PB-solvers 査読有り
Masahiko Sakai, Hidetomo Nabeshima
IEICE Transaction on Information and Systems E98-D 巻 ( 6 ) 頁： 1121-1127 2015年6月
詳細を見る
担当区分：筆頭著者 記述言語：英語 掲載種別：研究論文（学術雑誌）
-
Towards an Equational Theory of Rhythm Notation 査読有り
Pierre Donat-Bouillud, Florent Jacquemard, and Masahiko Sakai
Proc. of The Music Encoding Conference 2015 頁： 2 pages 2015年5月
詳細を見る
記述言語：英語
-
Non-E-overlapping and weakly shallow TRSs are confluent 査読有り
Masahiko Sakai, Michio Oyamaguchi, Mizuhito Ogawa
Proceedings of the 3rd International Workshop on Confluence (IWC 2014) 頁： 34-38 2014年7月
詳細を見る
担当区分：筆頭著者 記述言語：英語
-
Inverse Unfold Problem and Its Heuristic Solving 査読有り
Masanori Nagashima, Tomofumi Kato, Masahiko Sakai and Naoki Nishida
OASIcs 40 巻 頁： 27-38 2014年7月
詳細を見る
記述言語：英語
-
On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms 査読有り
Naoki Nishida, Masahiko Sakai, Yasuhiro Nakano
Electronic Proceedings in Theoretical Computer Science 134 巻 頁： 1-10 2013年10月
詳細を見る
-
Improving Determinization of Grammar Programs for Program Inversion 査読有り
Minami Niwa, Naoki Nishida, and Masahiko Sakai
Lecture Notes in Computer Science 7844 巻 頁： 137-154 2013年4月
詳細を見る
記述言語：英語 掲載種別：研究論文（学術雑誌）
-
Determinization of conditional term rewriting systems 招待有り 査読有り
Masanori Nagashima, Masahiko Sakai, Toshiki Sakabe
Theoretical Computer Science 464 巻 頁： 72-89 2012年12月
詳細を見る
記述言語：英語 掲載種別：研究論文（学術雑誌）
This paper discusses determinization of conditional term rewriting systems with oriented constructor rules. We present a rule-based transformation system, which transforms a non-deterministic one into a deterministic one, together with examples of the transformation. We prove that the transformation system is simulation sound and simulation complete. We also prove that the transformation system is complete for some class by introducing a strategy for the transformation system.
-
Extending Matching Operation in Grammar Program for Program Inversion 査読有り
Minami Niwa, Naoki Nishida, and Masahiko Sakai
Proceedings of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2012) 頁： 130-139 2012年9月
詳細を見る
記述言語：英語
-
Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity 査読有り
Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe
Logical Methods in Computer Science 8 巻 ( 3-4 ) 頁： 1-49 2012年8月
詳細を見る
-
On determinazation of conditional term rewriting systems 査読有り
Masahiko Sakai
Proc. of 9th Asian Workshop on Foundation of Software (AWFS 2012) 頁： 18-19 2012年6月
詳細を見る
担当区分：筆頭著者 記述言語：英語
-
Constrained Tree Automata and their Closure Properties 査読有り
Naoki Nishida, Futoshi Nomura, Katsuhisa Kurahashi and Masahiko Sakai
Proceedings of the 1st International Workshop on Trends in Tree Automata and Tree Transducers (TTATT 2012) 頁： 24-34 2012年6月
詳細を見る
記述言語：英語
-
A Sound Type System for Typing Runtime Errors 査読有り
YAMADA Akihisa, KUSAKARI Keiichirou, SAKABE Toshiki, SAKAI Masahiko, NISHIDA Naoki
IPSJ Transactions on Programming 頁： to appear 2012年3月
詳細を見る
記述言語：英語 掲載種別：研究論文（学術雑誌）
-
Controlled Term Rewriting 査読有り
Florent Jacquemard, KOJIMA Yoshiharu, and SAKAI Masahiko
Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FroCos 2011), LNCS 6989 巻 頁： 179-194 2011年10月
詳細を見る
記述言語：英語
-
Decidability of Reachability for Right-Shallow Context-Sensitive Term Rewriting Systems 査読有り
KOJIMA Yoshiharu, SAKAI Masahiko, NISHIDA Naoki, KUSAKARI Keiichirou, SAKABE Toshiki
IPSJ Transactions on Programming 4 巻 ( 4 ) 頁： 12-35 2011年9月
詳細を見る
記述言語：英語 掲載種別：研究論文（学術雑誌）
-
Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity 査読有り
NISHIDA Naoki, SAKAI Masahiko, SAKABE Toshiki
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), LIPIcs 10 巻 頁： 267-282 2011年5月
詳細を見る
記述言語：英語
-
例外処理を持つ関数型プログラムの停止性・非停止性証明法 査読有り
濱口 毅, 酒井正彦, 馬場正貴, 阿草清滋
4 巻 ( 2 ) 頁： 1-19 2011年3月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
制約付き項書換え系の書換え帰納法における補題等式の自動生成法 査読有り
中林直生, 西田直樹, 草刈圭一朗, 坂部俊樹, 酒井正彦
コンピュータソフトウェア 28 巻 ( 1 ) 頁： 173-189 2011年2月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
順方向ナローイングに基づく右線形右シャロー項書換え系の非停止性証明について
服部達哉、酒井正彦、西田直樹、草刈圭一朗、坂部俊樹
電子情報通信学会技術研究報告 110 巻 ( 336 ) 頁： 31-36 2010年12月
詳細を見る
記述言語：日本語
-
等式理論を法とするDPLL遷移系について
馬場達也、坂部俊樹、西田直樹、草刈圭一朗、酒井正彦
電子情報通信学会技術研究報告 110 巻 ( 227 ) 頁： 49-54 2010年10月
詳細を見る
記述言語：日本語
-
難解言語Malbolgeのチューリング完全性について
長坂 哲、酒井正彦、坂部俊樹、草刈圭一朗、西田直樹
電子情報通信学会技術研究報告 110 巻 ( 227 ) 頁： 55-60 2010年10月
詳細を見る
記述言語：日本語
-
Weakly-non-overlapping non-collapsing shallow term rewriting systems are confluent 査読有り
Masahiko Sakai, Mizuhito Ogawa
Information Processing Letters 110 巻 ( 18-19 ) 頁： 795-844 2010年9月
詳細を見る
担当区分：筆頭著者 記述言語：英語 掲載種別：研究論文（学術雑誌）
-
等式論理を法とする抽象DPLLアルゴリズムの提案
馬場達也、坂部俊樹、酒井正彦、草刈圭一朗、西田直樹
平成22年度電気関係学会東海支部連合大会講演論文集 頁： D3-4 2010年8月
詳細を見る
記述言語：日本語
-
制約付き項書換え系における関数の効率的な等価性検証
高桑一也、西田直樹、酒井正彦、坂部俊樹、草刈圭一朗
平成22年度電気関係学会東海支部連合大会講演論文集 頁： D3-6 2010年8月
詳細を見る
記述言語：日本語
-
2カウンタ法に基づく基本対称節を持つCNF論理式のSATソルバ
日野善信、酒井正彦、草刈圭一朗、坂部俊樹、西田直樹
平成22年度電気関係学会東海支部連合大会講演論文集 頁： D3-5 2010年8月
詳細を見る
記述言語：日本語
-
On Disproving Termiation of Constrained Term Rewriting Systems 査読有り
Naoki Nishida, Masahiko Sakai, Tatsuya Hattori
Proc. of Ninth International Workshop on Termination, (WST2010) 頁： 5 pages 2010年7月
詳細を見る
記述言語：英語
-
Decidability of Termination and Innermost Termination for Term Rewriting Systems with Right-Shallow Dependency Pairs 査読有り
UCHIYAMA Keita, SAKAI Masahiko, SAKABE Toshiki
IEICE Transaction on Information and Systems E93-D 巻 ( 5 ) 頁： 953-962 2010年5月
詳細を見る
記述言語：英語 掲載種別：研究論文（学術雑誌）
-
Proving Injectivity of Functions via Program Inversion in Term Rewriting. 査読有り
Naoki Nishida and Masahiko Sakai
Proceedings of the 10th International Symposium on Functional and Logic Programming (FLOPS 2010),Lecture Notes in Computer Science 6009 巻 頁： 288-303 2010年4月
詳細を見る
記述言語：英語
-
Decidability of Termination and Innermost Termination for Term Rewriting Systems with Right-Shallow Dependency Pairs 査読有り
Keita Uchiyama, Masahiko Sakai, Toshiki Sakabe
IEICE Trans. on Information and Systems E93-D 巻 ( 5 ) 頁： 953-962 2010年1月
詳細を見る
記述言語：英語 掲載種別：研究論文（学術雑誌）
-
基本対象関数に基づく節を持つCNF論理式の充足可能性判定 査読有り
馬野洋平, 酒井正彦, 西田直樹, 坂部俊樹, 草刈圭一朗
電子情報通信学会論文誌 J93-D 巻 ( 1 ) 頁： 1-9 2010年1月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
高階書換え系における引数切り落とし法と実効規則
鈴木翔、草刈圭一朗、坂部俊樹、酒井正彦、西田直樹
電子情報通信学会技術研究報告 109 巻 ( 343 ) 頁： 25-30 2009年12月
詳細を見る
記述言語：日本語
-
条件付き等式の変換に基づくプログラム生成
長島正憲，酒井正彦，坂部俊樹，西田直樹，草刈圭一朗
電子情報通信学会技術研究報告 109 巻 ( 343 ) 頁： 37-42 2009年12月
詳細を見る
記述言語：日本語
-
右線形右シャローな項書換え系における文脈依存停止性の決定可能性について
御宿義勝、酒井正彦、坂部俊樹、草刈圭一朗、西田直樹
電子情報通信学会技術研究報告 109 巻 ( 343 ) 頁： 31-36 2009年12月
詳細を見る
記述言語：日本語
-
Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems 査読有り
Yasuo Isogai, Keiichirou Kusakari, Masahiko Sakai, Frederic Blanqui
IEICE Trans. on Information and Systems E92-D 巻 ( 10 ) 頁： 235-247 2009年10月
詳細を見る
記述言語：英語 掲載種別：研究論文（学術雑誌）
-
制約付き項書換え系の書換え帰納法における補題等式の自動生成法
中林直生，西田直樹，草刈圭一朗，坂部俊樹，酒井正彦
日本ソフトウェア科学会 第26回大会論文集 7B-12 巻 頁： 1-14 2009年9月
詳細を見る
記述言語：日本語
-
Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems 査読有り
Yoshiharu Kojima, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, Toshiki Sakabe
IPSJ Transactions of Programming 2 巻 ( 3 ) 頁： 20-32 2009年7月
詳細を見る
記述言語：英語 掲載種別：研究論文（学術雑誌）
-
制約付き項書換え系における書換え帰納法 査読有り
坂田 翼, 西田 直樹, 酒井 正彦, 草刈 圭一朗, 坂部 俊樹
情報処理学会論文誌プログラミング 2 巻 ( 2 ) 頁： 80-96 2009年3月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
Recognizability of Redexes for Higher-Order Rewrite Systems 査読有り
Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa
IPSJ Transactions of Programming 2 巻 ( 2 ) 頁： 166-175 2009年3月
詳細を見る
記述言語：英語 掲載種別：研究論文（学術雑誌）
-
Head-Needed Strategy of Higher-Order Rewrite Systems and Its Decidable Classes 査読有り
Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa
IPSJ Transactions of Programming 2 巻 ( 2 ) 頁： 144-165 2009年3月
詳細を見る
記述言語：英語 掲載種別：研究論文（学術雑誌）
-
Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques 査読有り
Keiichirou Kusakari, Masahiko Sakai
IEICE Trans. on Information and Systems E92-D 巻 ( 2 ) 頁： 235-247 2009年2月
詳細を見る
記述言語：英語 掲載種別：研究論文（学術雑誌）
-
制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み 査読有り
古市 祐樹, 西田 直樹, 酒井 正彦, 草刈 圭一朗, 坂部 俊樹
情報処理学会論文誌プログラミング 1 巻 ( 2 ) 頁： 100-121 2008年9月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
*Innermost Reachability and Context Sensitive Reachability Properties are Decidable for Linear Right-Shallow Term Rewriting Systems 査読有り
Yoshiharu Kojima, Masahiko Sakai
Proc. of 19th Int'l Conference on Rewriting Techniqes and Applications, Hagenberg RTA2008, LNCS 5117 巻 頁： 187-201 2008年7月
詳細を見る
記述言語：英語
A reachability problem is a problem used to decide whether s is reachable to t by R or not for a given two terms s, t and a term rewriting system R. Since it is known that this problem is undecidable, effort has been devoted to finding subclasses of term rewriting systems in which the eachabilit
y is decidable. However few works on decidability exist for innermost reduction strategy or context-sensitive rewriting.
In this paper, we show that innermost reachability and
context-sensitive reachability are decidable for linear right-shallow term rewriting systems. Our approach is based on the tree automata technique that is commonly
used for analysis of reachability and its related properties. -
Completion as Post-Process in Program Inversion of Injective Functions 査読有り
Naoki Nishida, Masahiko Sakai
"Proc. of 8th International Workshop on Reduction Strategies in Rewriting and Programming, Hagenberg (WRS2008)" 頁： 61-75 2008年7月
詳細を見る
記述言語：英語
-
Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems 査読有り
Keita Uchiyama, Masahiko Sakai and Toshiki Sakabe
Electronic Notes in Theoretical Computer Science 204 巻 ( 4 ) 頁： 21-34 2008年4月
詳細を見る
記述言語：英語 掲載種別：研究論文（学術雑誌）
-
*Undecidable Properties on Length-Two String Rewriting Systems 査読有り
Masahiko Sakai and Wang Yi
Electronic Notes in Theoretical Computer Science 204 巻 ( 4 ) 頁： 53-69 2008年4月
詳細を見る
担当区分：筆頭著者 記述言語：英語 掲載種別：研究論文（学術雑誌）
Length-two string rewriting systems are length-preserving string rewriting systems that consist of length-two rules. This paper shows that confluence, termination, left-most termination and right-most termination are undecidable
properties for length-two string rewriting systems. These results mean that these properties are undecidable for
the class of linear term rewriting systems in which depth-two variables are allowed in both-hand sides of rules. -
Error Detection with Soft Typing for Dynamically Typed Language
"Akihisa Yamada, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, and Naoki Nishida"
IEICE Technical Report 107 巻 ( 505 ) 頁： 7-12 2008年3月
詳細を見る
記述言語：英語
-
例外処理付きオブジェクト指向プログラムにおける情報流の安全性解析のための型システム 査読有り
黒川翔, 桑原寛明, 山本晋一郎, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹
電子情報通信学会論文誌 J91-D 巻 ( 3 ) 頁： 757-770 2008年3月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
等式を規則化する変換の停止条件
水野清貴，西田直樹，坂部俊樹、酒井正彦，草刈圭一朗
電子情報通信学会技術研究報告 107 巻 ( 505 ) 頁： 25-30 2008年3月
詳細を見る
記述言語：日本語
-
Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques
"Keiichirou Kusakari, Masahiko Sakai"
IEICE Technical Report 107 巻 ( 505 ) 頁： 19-24 2008年3月
詳細を見る
記述言語：英語
-
プログラム生成系GeneSysにおける等式仕様への否定の導入
近藤悟、酒井正彦、坂部俊樹、草刈圭一朗、西田直樹
電子情報通信学会技術研究報告 107 巻 ( 392 ) 頁： 43-48 2007年12月
詳細を見る
記述言語：日本語
-
対話型埋込みによる数独問題の設計ツール
馬野洋平、酒井正彦、西田直樹、坂部俊樹、草刈圭一朗
電子情報通信学会技術研究報告 107 巻 ( 392 ) 頁： 73-78 2007年12月
詳細を見る
記述言語：日本語
-
導出木からのループ検出による論理プログラムの非停止性証明法
水谷知博、西田直樹、酒井正彦、坂部俊樹、草刈圭一朗、
電子情報通信学会技術研究報告 107 巻 ( 275 ) 頁： 1-6 2007年10月
詳細を見る
記述言語：日本語
-
*Enhancing Dependency Pair Method using Strong Computability in Simply-Typed Term Rewriting 査読有り
Keiichirou Kusakari, Masahiko Sakai
Applicable Algebra in Engineering, Communication and Computing 18 巻 ( 5 ) 頁： 407-431 2007年10月
詳細を見る
記述言語：英語 掲載種別：研究論文（学術雑誌）
We enhance the dependency pair method in order to prove termination using recursive structure analysis in simply-typed term rewriting systems, which is one of the computational models of functional programs. The primary advantage of our method is that one can exclude higher-order variables which are difficult to analyze theoretically, from recursive structure analysis. The key idea of our method is to analyze recursive structure from the viewpoint of strong computability. This property was introduced for proving termination in typed lambda-calculus, and is a stronger condition than the property of termination. The difficulty in incorporating this concept into recursive structure analysis is that because it is defined inductively over type structure, it is not closed under the subterm relation. This breaks the correspondence between strong computability and recursive structure. In order to guarantee the correspondence, we propose plain function-passing as a restriction, which is satisfied by
many non-artificial functional programs. -
論理式への変換に基づく魔方陣の発見
伊藤寛之、酒井正彦，草刈圭一朗，坂部俊樹，西田直樹
平成19年度電気関係学会東海支部連合大会講演論文集 頁： O-012 2007年9月
詳細を見る
記述言語：日本語
-
左線形は定向条件付き項書換え系における到達可能な項集合の近似集合を認識する木オートマトン
村田俊樹、西田直樹、酒井正彦、坂部俊樹、草刈圭一朗
電子情報通信学会技術研究報告 107 巻 ( 176 ) 頁： 1-6 2007年8月
詳細を見る
記述言語：日本語
-
振舞等価性の証明のための等式付き書換えに基づく潜在帰納法
笹田悠司、酒井正彦、西田直樹、坂部俊樹、草刈圭一朗
電子情報通信学会技術研究報告 107 巻 ( 176 ) 頁： 7-12 2007年8月
詳細を見る
記述言語：日本語
-
Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems 査読有り
"Keita Uchiyama, Masahiko Sakai and Toshiki Sakabe"
"Proc. of 7th International Workshop on Reduction Strategies in Rewriting and Programming, Paris (WRS2007)" 頁： 16-27 2007年6月
詳細を見る
記述言語：英語
-
Static Dependency Pair Method for Proving Termination of Higher-Order Rewriting Systems
"Kiichirou Kusakari, Yasuo Isogai, Masahiko Sakai, Toshiki Sakabe and Naoki Nishida"
107 巻 ( 99 ) 頁： 17-22 2007年6月
詳細を見る
記述言語：英語
-
二階の書換え系における引数切り落とし法
磯谷泰巨、草刈圭一朗、酒井正彦、坂部俊樹、西田直樹
電子情報通信学会技術研究報告 107 巻 ( 99 ) 頁： 23-28 2007年6月
詳細を見る
記述言語：日本語
-
Convergent Term Rewriting Systems for Inverse Computation of Injective Functions 査読有り
"WaNaoki Nishida, Masahiko Sakai, and Terutoshi Kato"
"Proc. of Ninth International Workshop on Termination, Paris (WST2007)" 頁： 77-81 2007年6月
詳細を見る
記述言語：英語
-
Undecidable Properties on Length-Two String Rewriting Systems 査読有り
Masahiko Sakai and Wang Yi
"Proc. of 7th International Workshop on Reduction Strategies in Rewriting and Programming, Paris (WRS2007)" 頁： 43-57 2007年6月
詳細を見る
担当区分：筆頭著者 記述言語：英語
-
Decidability of Innermost Termination for Semi-Constructor Term Rewriting Systems
"Keita Uchiyama, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe and Keiichirou Kusakari"
"RIMS Technical Report, Kyoto Universty" 1554 巻 頁： 166-170 2007年5月
詳細を見る
記述言語：英語
-
Confluence of Length Preserving String Rewriting System is Undecidable
"Yi Wang, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe and Keiichirou Kusakari"
"RIMS Technical Report, Kyoto Universty" 1554 巻 頁： 171-177 2007年5月
詳細を見る
記述言語：英語
-
単純型項書き換え系上の依存対法における実効規則と直積型項へのラベル付け 査読有り
櫻井敬大、草刈圭一朗、酒井正彦、坂部俊樹、西田直樹
電子情報通信学会論文誌 J90-D 巻 ( 4 ) 頁： 978-989 2007年4月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
単純型項書換え系における定理自動証明系HOPSYS
蒲田 明憲，草刈 圭一朗，西田 直樹，酒井 正彦，坂部 俊樹
電子情報通信学会技術研究報告 106 巻 ( 424 ) 頁： 7-12 2006年12月
詳細を見る
記述言語：日本語
-
手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み
古市祐樹，西田 直樹，酒井 正彦，草刈 圭一朗，坂部 俊樹
電子情報通信学会技術研究報告 106 巻 ( 324 ) 頁： 7-12 2006年10月
詳細を見る
記述言語：日本語
-
GeneSysによるプログラム生成例とIntroduction規則の追加
近藤 悟，酒井 正彦，西田 直樹，坂部 俊樹，草刈 圭一朗
電子情報通信学会技術研究報告 106 巻 ( 324 ) 頁： 37-42 2006年10月
詳細を見る
記述言語：日本語
-
例外処理付きオブジェクト指向言語における情報流の安全性解析
黒川 翔，桑原寛明，山本晋一郎，坂部俊樹，酒井正彦，草刈圭一朗，西田直樹
電子情報通信学会技術研究報告 106 巻 ( 324 ) 頁： 13-18 2006年10月
詳細を見る
記述言語：日本語
-
高階関数機能を持つ項書換え系のコンパイル
笹田悠司，酒井正彦，坂部俊樹，草刈圭一朗，西田直樹
平成18年度電気関係学会東海支部連合大会講演論文集 頁： O-437 2006年9月
詳細を見る
記述言語：日本語
-
所属制約を持つ条件付き項書換え系の紐解き変換
村田俊樹，西田直樹，酒井正彦，坂部俊樹，草刈圭一朗
平成18年度電気関係学会東海支部連合大会講演論文集 頁： O-438 2006年9月
詳細を見る
記述言語：日本語
-
*Decidability of Termination Left-Linear Shallow TRSs and Related Systems for Semi-Constructor TRSs 査読有り
Wang Yi and Masahiko Sakai
Proc. of 17th Int'l Conference on Rewriting Techniqes and Applications, Seattle RTA2006, LNCS 4098 巻 頁： 343-356 2006年8月
詳細を見る
記述言語：英語
"We consider several classes of term rewriting systems and prove that termination is decidable for these classes. By showing the cycling property of infinite dependency chains, we prove that termination is decidable for semi-constructor case, which is a superclass of right-ground TRSs. By analyzing argument propagation cycles in the dependency graph, we show that termination is also decidable for left-linear shallow TRSs. Moreover we extend these by combining these two techniques."
-
Transformation for Refining Unraveled Conditional Term Rewriting Systems 査読有り
"Naoki Nishida, Tomohiro Mizutani, and Masahiko Sakai"
"Proc. of 6th International Workshop on Reduction Strategies in Rewriting and Programming, Seattle (WRS2006)" 頁： 34-48 2006年8月
詳細を見る
記述言語：英語
-
On Non-looping Term Rewriting 査読有り
Wang Yi and Masahiko Sakai
"Proc. of Eighth International Workshop on Termination, Seattle (WST2006)" 頁： 17-21 2006年8月
詳細を見る
記述言語：英語
-
等式付き書換え系の等式数を削減する変換
三浦浩一，西田直樹，酒井正彦，坂部俊樹，草刈圭一朗
電子情報通信学会技術研究報告 106 巻 ( 120 ) 頁： 7-12 2006年6月
詳細を見る
記述言語：日本語
-
単純型項書換え系上の依存対法における実行規則と直積型項へのラベル付け
櫻井敬大，草刈圭一朗，酒井正彦，坂部俊樹，西田直樹
電子情報通信学会技術研究報告 106 巻 ( 120 ) 頁： 13-18 2006年6月
詳細を見る
記述言語：日本語
-
紐解かれた項書換え系の文脈依存条件の除去のための変換
"水谷知博，西田直樹, 酒井正彦,草刈圭一朗, 坂部俊樹"
京都大学数理解析研究所講究録 1489 巻 頁： 195-201 2006年5月
詳細を見る
記述言語：日本語
-
強計算依存対法による高階書換え系の停止性証明
磯谷泰巨，草刈圭一朗，酒井正彦，坂部俊樹，西田直樹
電子情報通信学会技術研究報告 106 巻 ( 15 ) 頁： 31-36 2006年4月
詳細を見る
記述言語：日本語
-
項正規表現に基づくSpi計算の機密性検証
"田代善彦, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹"
電子情報通信学会技術研究報告 105 巻 ( 596 ) 頁： 35-40 2006年2月
詳細を見る
記述言語：日本語
-
関数プログラムの停止性証明に関する辞書式経路順序
"星野由美, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹"
電子情報通信学会技術研究報告 105 巻 ( 597 ) 頁： 13-18 2006年2月
詳細を見る
記述言語：日本語
-
Primitive Indeuctive Theorems Bridge Implicit Induction methods and Inductive Theorems in Higher-Order Rewriting 査読有り
"Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe"
IEICE Trans. on Information and Systems E88-D 巻 ( 12 ) 頁： 2715-2726 2005年12月
詳細を見る
記述言語：英語 掲載種別：研究論文（学術雑誌）
-
Decidability of Termination fo Left-Linear Shallow Term Rewriting Systems and Related
"Yi Wang, Masahiko Sakai, Naoki Nishida, Keiichiro Kusakari, Toshiki Sakabe"
IEICE Technical Report 105 巻 ( 499 ) 頁： 9-13 2005年12月
詳細を見る
記述言語：英語
-
分散JoinJAVAプログラムの通信エラーに対する型判定システム
佐伯昌樹，坂部俊樹，酒井正彦，草刈圭一朗，西田直樹
電子情報通信学会技術報告 105 巻 ( 491 ) 頁： 25-30 2005年12月
詳細を見る
記述言語：日本語
-
強計算性による単純型項書換え系の依存対法の改良
105 巻 ( 491 ) 頁： 13-18 2005年12月
詳細を見る
記述言語：日本語
-
暗号プロトコル記述からカラーペトリネットへの変換による機密性検証
奥谷大介，坂部俊樹，酒井正彦，草刈圭一朗，西田直樹
電子情報通信学会技術報告 105 巻 ( 490 ) 頁： 19-24 2005年12月
詳細を見る
記述言語：日本語
-
重なりを持つTRSにおける最外戦略の完全性について
"岩田篤史，酒井正彦，西田直樹，草刈圭一朗, 西田直樹"
電子情報通信学会技術報告 SS2005-46 105 巻 ( 331 ) 頁： 39-44 2005年10月
詳細を見る
記述言語：日本語
-
カラーペトリネットを用いた暗号プロトコルの安全性検証
奥谷大介、坂部俊樹、酒井正彦、草刈圭一朗、西田直樹
平成17年度電気関係学会東海支部連合大会講演論文集 頁： O-198 2005年9月
詳細を見る
記述言語：日本語
-
分散JoinJAVAプログラムの正常実行判定のための型システム
佐伯昌樹、坂部俊樹、酒井正彦、草刈圭一朗、西田直樹
平成17年度電気関係学会東海支部連合大会講演論文集 頁： O-306 2005年9月
詳細を見る
記述言語：日本語
-
関数プログラムの再帰構造解析と強計算性に基づく十分完全性の証明法 査読有り
櫻井敬大、草刈圭一朗、西田直樹、酒井正彦、坂部俊樹
情報科学技術レターズ LA-001 巻 頁： 1-4 2005年9月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
構成子項書換え系の逆計算プログラムの生成 査読有り
西田直樹、酒井正彦、坂部俊樹
電子情報通信学会論文誌 J88-D-I 巻 ( 8 ) 頁： 1171-1183 2005年8月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
Decidability of Termination for Semi-Constructor Term Rewriting Systems
"Yi Wang, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, Toshiki Sakabe"
"Tech. Reort of IEICE, SS2005-27" 105 巻 ( 228 ) 頁： 13-18 2005年8月
詳細を見る
記述言語：英語
-
難読プログラミング言語Malbolgeにおけるプログラム構成手法
"飯澤 恒, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹"
電子情報通信学会技術報告 SS2005-22 巻 頁： 25-30 2005年6月
詳細を見る
記述言語：日本語
-
弱最内戦略を完全にする項書換え系の等価変換
"岡本晃治, 酒井正彦, 西田直樹, 草刈圭一朗"
京都大学数理解析研究所講究録 1426 巻 頁： 119-125 2005年4月
詳細を見る
記述言語：日本語
-
Partial Inversion of Constructor Term Rewriting Systems 査読有り
"Naoki Nishida, Masahiko Sakai, Toshiki Sakabe"
"Proc. of 16th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science" 3647 巻 頁： 264-278 2005年4月
詳細を見る
記述言語：英語
-
配列を扱う非線形先頭再帰プログラムからの再帰除去
"高須洋平, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹"
京都大学数理解析研究所講究録 1426 巻 頁： 39-44 2005年4月
詳細を見る
記述言語：日本語
-
項到達可能性の判定における成長TRSに対する手法と正規化規則による手法の関係
"村田龍彦, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹"
京都大学数理解析研究所講究録 1426 巻 頁： 106-112 2005年4月
詳細を見る
記述言語：日本語
-
変換と部分評価に基づく非左辺正規なメタ項の停止性証明
"蛸島洋明, 酒井正彦, 坂部俊樹, 西田直樹, 草刈圭一朗"
京都大学数理解析研究所講究録 1426 巻 頁： 113-118 2005年4月
詳細を見る
記述言語：日本語
-
On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems 査読有り
"Masahiko Sakai, Keiichirou Kusakari"
IEICE Trans. on Information and Systems E88-D 巻 ( 3 ) 頁： 583-593 2005年3月
詳細を見る
担当区分：筆頭著者 記述言語：英語 掲載種別：研究論文（学術雑誌）
-
項の全正規形を探索するためのTRSコンパイラ
岩田篤史、草刈圭一朗、酒井正彦、坂部俊樹
平成16年度電気関係学会東海支部連合大会講演論文集 頁： 363 2004年9月
詳細を見る
記述言語：日本語
-
項書換え系と木オートマトンを用いた共通鍵方式暗号プロトコルの検証法
奥谷大介、坂部俊樹、酒井正彦
平成16年度電気関係学会東海支部連合大会講演論文集 頁： 352 2004年9月
詳細を見る
記述言語：日本語
-
高階書換え系の決定可能な計算戦略について
粕谷英人、酒井正彦、阿草清滋
電子情報通信学会技術報告 SS2004-6 巻 頁： 1-6 2004年8月
詳細を見る
記述言語：日本語
-
On Simulation-Completeness of Unraveling for Conditional Term Rewriting Systems
"Naoki Nishida, Masahiko Sakai, Toshiki Sakabe"
Technical Report of IEICE SS2004-6 巻 頁： 25-30 2004年8月
詳細を見る
記述言語：英語
-
On Simulation-Completeness of Unraveling for Conditional Term Rewriting Systems
Naoki Nishida, Masahiko Sakai, Toshiki Sakabe
LA symposium 頁： 7.1-7.6 2004年7月
詳細を見る
記述言語：英語
-
限量子付き等式理論の変換に基づく仕様からのプログラム生成 査読有り
長島正徳、酒井正彦、坂部俊樹、草刈圭一朗
コンピュータソフトウェア 21 巻 ( 4 ) 頁： 49-54 2004年7月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
本論文では、既知関数を記述する項書換え系と生成したい未知関数の仕様を論理式の集合とみなして、その変換に基づくプログラム自動生成を試みる。まず、等式と論理和・論理積・限量子からなる論理式の集合を対象とする変換系を提案する。次に、変換により得られた論理式集合から元の論理式集合の全ての論理式が証明可能であることを示す。このことは、変換によって得られた論理式集合が実行可能なプログラムとみなせるときに、そのプログラムが仕様を満足することを保障している。最後に、プログラム自動生成の一例を挙げる。
-
左辺が一致するオーバレイ性を持つ左線形ＴＲＳの正規化戦略
水野健一、草刈圭一朗、酒井正彦、坂部俊樹
京都大学数理解析研究所講究録 1375 巻 頁： 247-252 2004年5月
詳細を見る
記述言語：日本語
-
右辺のみに現れる変数を持つ線形構成子項書換え系の計算の効率化 査読有り
西田直樹、酒井正彦、坂部俊樹
コンピュータソフトウェア 21 巻 ( 3 ) 頁： 40-47 2004年5月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
非完全な仕様における振舞等価性の自動証明法
山本友和、草刈圭一朗、酒井正彦、坂部俊樹
電子情報通信学会技術報告 COMP2003 巻 ( 66 ) 頁： 29-36 2003年12月
詳細を見る
記述言語：日本語
-
Characterizing Inductive Theorems by Extensional Initial Models in a Higher-Order Equational Logic
"Keiichiro Kusakari, Masahiko Sakai, Toshiki Sakabe"
46 巻 ( 9 ) 2003年10月
詳細を見る
記述言語：英語
-
メタ項書き換え計算における左辺正規性を持つメタ項の停止性について、
蛸島洋明、酒井正彦、坂部俊樹
平成15年度電気関係学会東海支部連合大会講演論文集 頁： 565 2003年10月
詳細を見る
記述言語：日本語
-
最内書換えに基づく項書換え系の完全な書換え戦略
岡本晃治、酒井正彦、坂部俊樹
平成15年度電気関係学会東海支部連合大会講演論文集 頁： 564 2003年10月
詳細を見る
記述言語：日本語
-
右辺のみに現れる変数を持つ項書換え系の計算モデル 査読有り
西田直樹、酒井正彦、坂部俊樹
コンピュータソフトウェア 20 巻 ( 5 ) 頁： 85-89 2003年9月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
右辺のみに現れる変数を持つ右線形構成子項書換え系の計算の効率化
西田直樹、酒井正彦、坂部俊樹
日本ソフトウェア科学会 第20回大会論文集 441-445 巻 2003年9月
詳細を見る
記述言語：日本語
-
高階項書換え系の決定可能性問題のためのNk木オートマトンとその性質、
粕谷英人、酒井正彦、阿草清滋
日本ソフトウェア科学会 第20回大会論文集 頁： 436-440 2003年9月
詳細を見る
記述言語：日本語
-
限量子付き等式理論の変換に基づく仕様からのプログラム生成、
長島正徳、酒井正彦、坂部俊樹、草刈圭一朗
日本ソフトウェア科学会 第20回大会論文集 頁： 431-435 2003年9月
詳細を見る
記述言語：日本語
-
右辺のみに現れる変数を持つ右線形オーバーレイ項書換え系の最左最内ナローイングによる正規形の計算
西田直樹、酒井正彦、坂部俊樹
2003年度夏のLAシンポジウム 頁： 24.1-24.6 2003年8月
詳細を見る
記述言語：日本語
-
右辺のみに現れる変数を持つ右線形オーバーレイ項書換え系の最左最内ナローイングによる正規形の計算
西田直樹、酒井正彦、坂部俊樹
2003年度夏のLAシンポジウム 頁： 24.1-24.6 2003年8月
詳細を見る
記述言語：日本語
-
Innermost Reductions Find All Normal Forms on Right-Linear Terminating Overlay TRSs 査読有り
"Masahiko Sakai, Kouji Okamoto, Toshiki Sakabe"
Proc. of 3rd Int'l Workshop on Reduction Strategies in Rewriting and Programming WRS'03 巻 頁： 79-88 2003年6月
詳細を見る
担当区分：筆頭著者 記述言語：英語
-
Narrowing-based Simulation of Term Rewriting Systems with Extra Variables and its Termination Proof 査読有り
"Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe"
Proc. of 12th Int'l Workshop on Functional and (Constraint) Logic Programming WFLP'03 巻 頁： 198-211 2003年6月
詳細を見る
担当区分：筆頭著者 記述言語：英語
-
右辺のみに現れる変数を持つ項書換え系のナローイングに基づく 実効的書き換えとその停止性
西田直樹、酒井正彦、坂部俊樹
京都大学数理解析研究所講究録 1325 巻 頁： 238-243 2003年5月
詳細を見る
記述言語：日本語
-
再帰型をもつオブジェクト指向計算モデルにおける例外処理の型付
堀江美保子、酒井正彦、坂部俊樹
京都大学数理解析研究所講究録 1325 巻 頁： 104-109 2003年5月
詳細を見る
記述言語：日本語
-
オブジェクト指向計算モデルにおける例外処理機能の型付 査読有り
堀江美保子、酒井正彦、坂部俊樹
コンピュータソフトウェア 20 巻 ( 2 ) 頁： 54-58 2003年3月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
Descendants and Head Normalization of Higher-Order Rewrite Systems 査読有り
"Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa"
Lecture Notes in Computer Science 2441 巻 2002年9月
詳細を見る
記述言語：英語
-
On Proving Termination of Higher-Order Rewrite Systems by Dependency Pair technique 査読有り
"Masahiko Sakai, Keiichirou Kusakari"
"Proc. of the First International Workshop on Higher-Order Rewriting (HOR'02), Copenhagen, Denmark" 頁： 25 2002年7月
詳細を見る
担当区分：筆頭著者 記述言語：英語
-
PT関数の逆関数を定義するTRSの生成 査読有り
西田直樹、酒井正彦、坂部俊樹
コンピュータソフトウェア 19 巻 ( 1 ) 頁： 29-33 2002年1月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
優先順序付き項書換え系の頭必須戦略の決定可能性
鈴木剛、酒井正彦、坂部俊樹
電子情報通信学会技術報告 COMP2001-80 巻 頁： 49-55 2002年1月
詳細を見る
記述言語：日本語
-
潜在帰納法による弱完全振舞仕様に対する振舞等価性の自動証明
加納康資、酒井正彦、坂部俊樹
電子情報通信学会技術報告 COMP2001-79 巻 頁： 41-47 2002年1月
詳細を見る
記述言語：日本語
-
高階書換え系におけるディセンダントと頭必須書換えの頭正規化性
粕谷英人、酒井正彦、阿草清滋
電子情報通信学会技術報告 COMP2001-82 巻 頁： 65-72 2002年1月
詳細を見る
記述言語：日本語
-
n箇所パターン照合関数のDeforestationに基づく効率化
中村敏広、酒井正彦、坂部俊樹
シンポジウム，情報基礎理論ワークショップ 2002年
詳細を見る
記述言語：日本語
-
n箇所パターン照合関数のDeforestationに基づく効率化
中村敏広、酒井正彦、坂部俊樹
シンポジウム，情報基礎理論ワークショップ 2002年
詳細を見る
記述言語：日本語
-
Generation of a TRS Implementing the Inverses of the Functions with Specified Arguments Fixed
"Naoki Nishida, Masahiko Sakai, Toshiki Sakabe"
Technical Report of IEICE COMP2001-67 巻 頁： 33-40 2001年12月
詳細を見る
記述言語：英語
-
Generation of Inverse Term Rewriting Systems for Pure Treeless Functions 査読有り
"Naoki Nishida, Masahiko Sakai, Toshiki Sakabe"
"Proc. of the International workshop on Rewriting in Proof and Computaion, Sendai, Japan" 頁： 188-198 2001年10月
詳細を見る
記述言語：英語
-
On New Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems 査読有り
"Masahiko Sakai, Keiichirou Kusakari"
"Proc. of the International Workshop on Rewriting in Proof and Computation (RPC'01), Sendai, Japan" 頁： 176-187 2001年10月
詳細を見る
担当区分：筆頭著者 記述言語：英語
-
An Extension of Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems 査読有り
"Masahiko Sakai, Yoshitsugu Watanabe, Toshiki Sakabe"
IEICE Trans. on Information and Systems E84-D 巻 ( 8 ) 頁： 1025-1032 2001年8月
詳細を見る
担当区分：筆頭著者 記述言語：英語 掲載種別：研究論文（学術雑誌）
-
PT関数の逆関数を定義する条件付きTRSの生成
西田直樹、酒井正彦、坂部俊樹
電子情報通信学会技術報告 COMP2001-14 巻 頁： 9-16 2001年6月
詳細を見る
記述言語：日本語
-
メタ項書換え計算における規則中に規則を含む直交メタ項の合流性 査読有り
洪順姫、酒井正彦、坂部俊樹
コンピュータソフトウェア 17 巻 ( 6 ) 頁： 47-51 2000年11月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
ユーザにごみ集めを意識させないCライブラ リの設計法
西田直樹、酒井正彦、坂部俊樹
電子情報通信学会技術報告 SS2000-9 巻 頁： 25-32 2000年5月
詳細を見る
記述言語：日本語
-
Confluence of Weakly Orthogonal CTRSs with Extra Variables
Ould Seyid Ahmed, Masahiko Sakai, Toshiki Sakabe
LA symposium 2000年
詳細を見る
記述言語：英語
-
Confluence of Weakly Orthogonal CTRSs with Extra Variables
"Ould Seyid Ahmed, Masahiko Sakai, Toshiki Sakabe"
LA symposium 2000年
詳細を見る
記述言語：英語
-
直交メタ項書換え計算のデベロップメントと合流性
洪順姫、酒井正彦、坂部俊樹
電子情報通信学会技術報告 COMP99-9 巻 頁： 65-70 1999年4月
詳細を見る
記述言語：日本語
-
順序ソートの自動推論とラベル付けに基づく合流性判定への応用
宮下大、酒井正彦、坂部俊樹
計算モデルとアルゴリズム、数理解析研究所講究録 1093 巻 頁： 136-141 1999年2月
詳細を見る
記述言語：日本語
-
項集合書換え系の完備化について
粕谷英人、酒井正彦、山本晋一郎、阿草清滋
電子情報通信学会技術報告 SS98-66 巻 頁： 25-31 1998年12月
詳細を見る
記述言語：日本語
-
Semantics and Strong Sequentiality of Priority Term Rewriting Systems 査読有り
"Masahiko Sakai, Yoshihito Toyama"
Theoretical Computer Science 208 巻 頁： 87-110 1998年11月
詳細を見る
担当区分：筆頭著者 記述言語：英語 掲載種別：研究論文（学術雑誌）
-
An Improved Recursive Decomposition Ordering for Higher-Order Rewrite Systems 査読有り
"Munehiro Iwami, Masahiko Sakai, Yoshihito Toyama"
IEICE Trans. on Information and Systems E81-D 巻 ( 9 ) 頁： 988-996 1998年9月
詳細を見る
記述言語：英語 掲載種別：研究論文（学術雑誌）
-
Index Reduction of Overlapping Strongly Sequential Systems 査読有り
"Takashi Nagaya, Masahiko Sakai, Yoshihito Toyama"
IEICE Trans. on Information and Systems E81-D 巻 ( 5 ) 頁： 419-426 1998年5月
詳細を見る
記述言語：英語 掲載種別：研究論文（学術雑誌）
-
項書換え系の拡張された階層的結合における停止性のモジュラー性
大野健治、河口信夫、酒井正彦、坂部俊樹、稲垣康善
電子情報通信学会技術報告 SS97-84 巻 頁： 57-61 1998年3月
詳細を見る
記述言語：日本語
-
依存対に基づく高階項書換え系の停止性証明
渡辺啓嗣、河口信夫、酒井正彦、坂部俊樹、稲垣康善
電子情報通信学会技術報告 SS97-85 巻 頁： 63-70 1998年3月
詳細を見る
記述言語：日本語
-
IIn型条件付き書換え系の合流性について
西村徹、酒井正彦、坂部俊樹
電子情報通信学会技術報告 COMP97-84 巻 頁： 45-49 1998年1月
詳細を見る
記述言語：日本語
-
Left-Incompatible Term Rewriting Systems and Functional Strategy 査読有り
Masahiko Sakai
IEICE Trans. on Information and Systems E80-D 巻 ( 12 ) 頁： 1176-1182 1997年12月
詳細を見る
担当区分：筆頭著者 記述言語：英語 掲載種別：研究論文（学術雑誌）
-
項集合書換え系とその合流性 査読有り
粕谷英人，酒井正彦，山本晋一郎，阿草清滋
電子情報通信学会誌 J80-D-I 巻 ( 4 ) 頁： 325-334 1997年4月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
An Improved Recursive Decomposition Ordering for Higher-Order Rewrite Systems
"Munehiro Iwami, Masahiko Sakai, Yoshihito Toyama"
"Tech. Rep., IEICE" COMP96-73 巻 頁： 17-24 1997年1月
詳細を見る
記述言語：英語
-
条件付き書換え系の合流性について 査読有り
高橋宜孝，酒井正彦，外山芳人
電子情報通信学会誌 J79-D-I 巻 ( 11 ) 頁： 897-902 1996年11月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
Semantics and Strong Sequentiality of Priority Term Rewriting Systems 査読有り
"Masahiko Sakai, Yoshihito Toyama"
"Proc. on Rewriting Techniques and Applications at New Brunswick NJ USA, LNCS" 1103 巻 頁： 377-391 1996年7月
詳細を見る
担当区分：筆頭著者 記述言語：英語
-
Index reduction of Overlapping Strong Sequential Systems
"Takashi Nagaya, Masahiko Sakai, Yoshihito Toyama"
"Tech. Rep., IEICE" COMP96-32 巻 頁： 39-48 1996年7月
詳細を見る
記述言語：英語
-
Church-Rosser Property of Finite Ranked Terms of Non-Linear Term Rewriting Systems
"Keiichiro Kusakari, Masahiko Sakai, Yoshihito Toyama"
LA Symposium 頁： 160-165 1996年7月
詳細を見る
記述言語：英語
-
Index reduction of Overlapping Strong Sequential Systems
"Takashi Nagaya, Masahiko Sakai, Yoshihito Toyama"
LA Symposium 頁： 154-165 1996年7月
詳細を見る
記述言語：英語
-
高階項書換え系の停止性について
岩見宗弘，酒井正彦，外山芳人
シンポジウム，情報基礎理論ワークショップ 頁： 55-60 1996年7月
詳細を見る
記述言語：日本語
-
項書換え系のAC停止性について
中野賢司，酒井正彦，外山芳人
電子情報通信学会技術報告 COMP95-104 巻 頁： 69-78 1996年3月
詳細を見る
記述言語：日本語
-
NVNF-sequeentiality of Left-linear Term Rewriting Systems
"Takashi Nagaya, Masahiko Sakai, Yoshihito Toyama"
"Kyokyuroku, Kyoto University" 950 巻 頁： 153-159 1996年2月
詳細を見る
記述言語：英語
-
高階項書換え系の停止性について
岩見宗弘，酒井正彦，外山芳人
電子情報通信学会技術報告 COMP95-85 巻 頁： 113-121 1996年1月
詳細を見る
記述言語：日本語
-
非線形項書換え系の合流性について
草刈圭一朗，酒井正彦，外山芳人
電子情報通信学会技術報告 COMP95-86 巻 頁： 123-129 1996年1月
詳細を見る
記述言語：日本語
-
The Semantics of Priority Term Rewriting Systems and their Strong Sequentiality
"Masahiko Sakai, Yoshihito Toyama"
"Technical report, IEICE" SS95-40 巻 頁： 31-38 1996年1月
詳細を見る
担当区分：筆頭著者 記述言語：英語
-
The Functional Strategy: the Extended Left-incompatible Systems
Masahiko Sakai
"Technical Report, IEICE" SS95-17 巻 頁： 55-62 1995年7月
詳細を見る
担当区分：筆頭著者 記述言語：英語
-
NVNF-sequeentiality of Left-linear Term Rewriting Systems
"Takashi Nagaya, Masahiko Sakai, Yoshihito Toyama"
"Proc. of RIMS Workshop on Theory of Rewriting Systems and its Applications, Kyokyuroku, Kyoto University" 918 巻 頁： 109-117 1995年7月
詳細を見る
記述言語：英語
-
共有メモリ型並列計算機における項書換え系の実現方式 査読有り
山本晋一郎，石川亮，酒井正彦，阿草清滋
電子情報通信学会論文誌 J78-D-I 巻 ( 6 ) 頁： 559-562 1995年6月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
形式的仕様を用いた再利用モデル 査読有り
川北誠，酒井正彦，山本晋一郎，阿草清滋
情報処理学会論文誌 36 巻 ( 5 ) 頁： 1050-1058 1995年5月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
エラーつき代数的仕様とエラー記述の自動付加 査読有り
"濱口 毅, 酒井 正彦, 山本 晋一郎, 阿草 清滋"
電子情報通信学会論文誌 J78-D-I 巻 ( 3 ) 頁： 323-330 1995年3月
詳細を見る
記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
項書換え系の合流性を保存する合併条件について
北原彰，酒井正彦，外山芳人
情報処理学会，プログラミング -言語・基礎・実践- 研究会 20 巻 ( 2 ) 頁： 11-20 1995年1月
詳細を見る
記述言語：日本語
-
仕様に基づく部品再利用法とその適用
川北誠，酒井正彦，山本晋一郎，阿草清滋
第1回ソフトウェア工学の基礎 ワークショップ FOSE94 巻 1994年12月
詳細を見る
記述言語：日本語
-
条件つき項書換え系の合流性について
高橋宜孝，酒井正彦，外山芳人
電子情報通信学会技術報告 COMP94-65 巻 頁： 105-111 1994年11月
詳細を見る
記述言語：日本語
-
NVNF-逐次系におけるインデックスの決定可能性
長谷崇，酒井正彦，外山芳人
電子情報通信学会，コンピュテーション研究会 COMP94-63 巻 頁： 87-94 1994年11月
詳細を見る
記述言語：日本語
-
項集合書換え系の合流性について
粕谷英人，酒井正彦，山本晋一郎，阿草清滋
電子情報通信学会，ソフトウェアサイエンス研究会 SS94-14 巻 頁： 17-24 1994年7月
詳細を見る
記述言語：日本語
-
On Term Set Rewriting System
"Masahiko Sakai, Hideto Kasuya, Shinichiro Yamamoto and Kiyoshi Agusa"
LA Symposium 頁： 45-48 1994年7月
詳細を見る
担当区分：筆頭著者 記述言語：英語
-
Similarity on Algebraic Specifications toward Specification Databases
Masahiko Sakai
"Technical Report, JAIST" IS-RR-94-0012S 巻 頁： 1-20 1994年5月
詳細を見る
担当区分：筆頭著者 記述言語：英語
-
項の集合の書換え系とKnuth-Bendixの完備化に関する考察
粕谷英人，酒井正彦，山本晋一郎，阿草清滋
電子情報通信学会，ソフトウェアサイエンス研究会 SS93-41 巻 頁： 17-22 1994年1月
詳細を見る
記述言語：日本語
-
ソフトウェア操作言語の提案
吉田敦，山本晋一郎，酒井正彦，阿草清滋
電子情報通信学会，ソフトウェアサイエンス研究会 SS92-18 巻 頁： 1-8 1993年1月
詳細を見る
記述言語：日本語
-
代数的仕様へのエラー記述の自動付加について
濱口毅，酒井正彦，山本晋一郎，阿草清滋
電子情報通信学会，ソフトウェアサイエンス研究会 SS92-26 巻 頁： 25-32 1993年1月
詳細を見る
記述言語：日本語
-
代数的仕様の検証のための被覆集合帰納法 査読有り
酒井正彦，坂部俊樹，稲垣康善
電子情報通信学会論文誌 J75-D-I 巻 ( 3 ) 頁： 170-179 1992年3月
詳細を見る
担当区分：筆頭著者 記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
Similarity on Algebraic Specifications toward Specification Databases
"Masahiko Sakai, Soichi Matsui, Shinichiro Yamamoto, Kiyoshi Agusa"
LA Symposium 頁： 30-35 1992年2月
詳細を見る
担当区分：筆頭著者 記述言語：英語
-
代数的仕様の検証のための被覆集合帰納法
酒井正彦，坂部俊樹，稲垣康善
情報基礎理論ワークショップ，LAシンポジュウム 頁： 12-17 1991年2月
詳細を見る
担当区分：筆頭著者 記述言語：日本語
-
コンパイラの代数的仕様記述と自動生成 査読有り
酒井正彦，坂部俊樹，稲垣康善
電子情報通信学会論文誌 J73-D-I 巻 ( 12 ) 頁： 979-989 1990年12月
詳細を見る
担当区分：筆頭著者 記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
代数的仕様記述法に基づく言語処理系の自動生成システムLass 査読有り
酒井正彦，坂部俊樹，稲垣康善
電子情報通信学会論文誌 J73-D-1 巻 ( 10 ) 頁： 829-838 1990年10月
詳細を見る
担当区分：筆頭著者 記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
代数的仕様の検証のための被覆集合帰納法
酒井正彦，坂部俊樹，稲垣康善
電子情報通信学会，コンピュテーション研究会 COMP90-5 巻 1990年5月
詳細を見る
担当区分：筆頭著者 記述言語：日本語
-
コンパイル機能を持つTRSインタプリタの実現
酒井正彦，坂部俊樹，稲垣康善
電子情報通信学会，コンピュテーション研究会 COMP88-93 巻 1989年2月
詳細を見る
担当区分：筆頭著者 記述言語：日本語
-
TRSインタプリタの並列最外戦略実現法
山本晋一郎，酒井正彦，坂部俊樹，稲垣康善
電子情報通信学会，コンピュテーション研究会 COMP88-94 巻 1989年2月
詳細を見る
記述言語：日本語
-
代数的仕様における帰納的性質の証明法
酒井正彦，坂部俊樹，稲垣康善
電子情報通信学会，コンピュテーション研究会 COMP88-86 巻 頁： 83-92 1989年1月
詳細を見る
担当区分：筆頭著者 記述言語：日本語
-
抽象データ型の代数的仕様の直接実現系Cdimple 査読有り
酒井正彦，坂部俊樹，稲垣康善
コンピュータソフトウェア 4 巻 ( 4 ) 頁： 16-27 1987年10月
詳細を見る
担当区分：筆頭著者 記述言語：日本語 掲載種別：研究論文（学術雑誌）
-
An Algebraic Approach to Specification of Programming Languages and Automatic Generation of Language Processors 査読有り
"Yasuyoshi Inagaki, Hidehiko Kita, Masahiko Sakai, Toshiki Sakabe"
Proceedings of Regional Symposium on Computer Science and its Applications in Thai 頁： 35-1-35-25 1987年1月
詳細を見る
記述言語：英語
-
抽象データ型の代数的仕様の直接実現系Cdimple
酒井正彦，坂部俊樹，稲垣康善
電子通信学会技術研究報告，コンピュテーション研究会 COMP96-67 巻 頁： 61-69 1987年1月
詳細を見る
担当区分：筆頭著者 記述言語：日本語
-
An Algebraic Approach to Specification of Programming Languages and Automatic Generation of Language Processors
"Yasuyoshi Inagaki, Hidehiko Kita, Masahiko Sakai, Toshiki Sakabe"
"Technical Research Report, Nagoya University" 8601 巻 1986年11月
詳細を見る
記述言語：英語
-
抽象データ型直接実現システムCdimple
酒井正彦，坂部俊樹，稲垣康善
ソフトウエア科学会，関数的プログラミング研究会 FP-86-07 巻 頁： 122-127 1986年11月
詳細を見る
担当区分：筆頭著者 記述言語：日本語
-
コンパイラの代数的仕様記述とその自動生成
酒井正彦，坂部俊樹，稲垣康善
情報処理学会研究報告，プログラミング言語研究会 86-PL-8-1 巻 頁： 1-9 1986年10月
詳細を見る
担当区分：筆頭著者 記述言語：日本語
-
コンパイラの代数的仕様記述法
酒井正彦，坂部俊樹，稲垣康善
電子通信学会技術研究報告，ソフトウエアサイエンス研究会 SS86-9 巻 頁： 1-6 1986年7月
詳細を見る
担当区分：筆頭著者 記述言語：日本語
-
代数的手法に基づくプログラミング言語の仕様記述法と処理系の自動生成
稲垣康善，北英彦，酒井正彦，坂部俊樹
情報処理学会，知識情報処理シンポジウム論文集 頁： 165-174 1985年9月
詳細を見る
記述言語：日本語
-
プログラミング言語の代数的仕様記述からのコンパイラ自動生成に関する基礎的考察
酒井正彦，北英彦，坂部俊樹，稲垣康善
言語理論とオートマトン理論シンポジウム論文集 頁： 98-101 1985年7月
詳細を見る
担当区分：筆頭著者 記述言語：日本語
-
プログラミング言語の代数的仕様記述からのコンパイラ自動生成
酒井正彦，北英彦，坂部俊樹，稲垣康善
電子通信学会技術研究報告，オートマトンと言語研究会 AL85-10 巻 頁： 1-10 1985年5月
詳細を見る
担当区分：筆頭著者 記述言語：日本語
MISC
MISC 3
-
Solving Rep-tile by Computers: Performance of Solvers and Analyses of Solutions
Mutsunori Banbara, Kenji Hashimoto, Takashi Horiyama, Shin-ichi Minato, Kakeru Nakamura, Masaaki Nishino, Masahiko Sakai, Ryuhei Uehara, Yushi Uno, Norihito Yasuda
arXiv 2110.05184 2021年6月
詳細を見る
担当区分：最終著者 記述言語：英語
-
Reduced dependency spaces for existential parameterised Boolean equation system 査読有り
Yutaro Nagae, Masahiko Sakai
Informal Proceedings of the 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017) 頁： 10 2017年9月
詳細を見る
記述言語：英語
-
Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers 査読有り
Tomohiro Sasano, Naoki Nishida, Masahiko Sakai, and Tomoya Ueyama
Informal Proceedings of the 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017) 頁： 10 2017年9月
詳細を見る
記述言語：英語
講演・口頭発表等
講演・口頭発表等 53
-
小栗 滉介, 酒井正彦, 橋本健二
組合せゲーム・パズル(CGP) プロジェクト, 第18回 研究集会 2024年3月
詳細を見る
開催年月日： 2024年3月
記述言語：日本語 会議種別：口頭発表（一般）
開催地：調布市
-
Ground Canonical Rewrite Systems Revisited 国際共著 国際会議
Aart Middeldorp, Masahiko Sakai, and Sarah Winkler
12th International Workshop on Confluence (IWC 2023) 2023年8月24日
詳細を見る
開催年月日： 2023年8月
記述言語：英語 会議種別：口頭発表（一般）
開催地：Obergurgl 国名：オーストリア共和国
-
Takeshi Hamaguchi, Masahiko Sakai
Technical report of IEICE, SS group 2023年1月11日
詳細を見る
開催年月日： 2023年1月
記述言語：英語 会議種別：口頭発表（一般）
開催地：Osaka 国名：日本国
-
自動演奏への表情付けのための生成音楽理論に基づくフレーズ情報の生成法
後藤 円香, 酒井 正彦, 東条 敏
第135回音楽情報科学研究発表会 2022年9月15日 情報処理学会
詳細を見る
開催年月日： 2022年9月
記述言語：日本語 会議種別：口頭発表（一般）
開催地：オンライン
-
番原睦則, 橋本健二, 堀山貴史, 湊真一, 中村駆, 西野正彬, 酒井正彦, 上原隆平, 宇野裕之, 安田宜仁
組合せゲーム・パズル(CGP) プロジェクト, 第16回 研究集会
詳細を見る
開催年月日： 2022年3月
記述言語：日本語 会議種別：口頭発表（一般）
開催地：オンライン
-
Equivalence of Context-Free and Regular Languages on Commutative Strings 国際会議
Masahiko Sakai
the 56th TRS meeting 2022年2月24日
詳細を見る
開催年月日： 2022年2月
記述言語：英語 会議種別：口頭発表（一般）
開催地：Nagoya/online 国名：日本国
-
命題論理式の全ての投射モデルを表現するBDDの構成法
磯貝孝明, 橋本健二, 酒井正彦
第116回人工知能基本問題研究会 2021年3月22日 人工知能学会
詳細を見る
開催年月日： 2021年3月
記述言語：日本語 会議種別：口頭発表（一般）
開催地：オンライン
-
計数セマフォを含むプログラムから論理制約付き項書換え系への変換
小嶋美咲, 西田直樹, 酒井正彦
情報処理学会第83回全国大会 2020年3月20日 情報処理学会
詳細を見る
開催年月日： 2021年3月
記述言語：日本語
開催地：オンライン
-
擬ブール制約の導入による組合せ最適化ソルバCombSQL+の高速化
岸潤一郎, 酒井正彦, 西田直樹, 橋本健二
ソフトウェアサイエンス研究会 2021年1月27日 電子情報通信学会
詳細を見る
開催年月日： 2021年1月
記述言語：日本語 会議種別：口頭発表（一般）
開催地：オンライン 国名：日本国
-
ASAP: a dataset of aligned scores and performances for piano transcription 国際共著 国際会議
Francesco Foscarin, Andrew McLeod, Philippe Rigaux, Florent Jacquemard, Masahiko Sakai
the 21st International Society for Music Information Retrieval Conference (ISMIR 2020) 2020年10月
詳細を見る
開催年月日： 2020年10月
記述言語：英語 会議種別：口頭発表（一般）
-
Transformation of SQL-based Combinatorial Optimization Problems into Constraint Problems
2020年9月30日 人工知能学会
詳細を見る
開催年月日： 2020年9月
会議種別：口頭発表（一般）
開催地：オンライン 国名：日本国
-
On Decision Diagrams
Masahiko Sakai
the 52nd TRS meeting
詳細を見る
開催年月日： 2020年2月
記述言語：英語 会議種別：口頭発表（一般）
開催地：Kaga, Ishikawa 国名：日本国
-
Rhythm quantization as an efficiently-solvable optimization problem
Masahiko Sakai
the 51st TRS meeting
詳細を見る
開催年月日： 2019年9月
記述言語：英語 会議種別：口頭発表（一般）
開催地：Sounkyo, Hokkaido 国名：日本国
-
SQL for combinatorial optimization problems and SMT-based solving by SQL transformation 招待有り 国際会議
Masahiko Sakai
Sixth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2019)
詳細を見る
開催年月日： 2019年6月
記述言語：英語 会議種別：口頭発表（一般）
開催地：Dortmund 国名：ドイツ連邦共和国
-
An extended SQL for combinatorial optimization problems and transformation into constraint problems
Masahiko Sakai
the 49th TRS meeting
詳細を見る
開催年月日： 2018年9月
記述言語：英語 会議種別：口頭発表（一般）
開催地：Ikaho, Gunma 国名：日本国
-
Transformation of combinatorial optimization problems written in extended SQL into constraint problems
Genki Sakanashi, Masahiko Sakai
IPSJ-SIGPRO
詳細を見る
開催年月日： 2018年6月
記述言語：英語 会議種別：口頭発表（一般）
開催地：Gifu 国名：日本国
-
On Confluence of Innermost Terminating Term Rewriting Systems
Masahiko Sakai
the 47th TRS meeting
詳細を見る
開催年月日： 2017年9月
記述言語：英語 会議種別：口頭発表（一般）
開催地：Matsue, Shimane 国名：日本国
-
On Confluence of Innermost Terminating Term Rewriting Systems 招待有り 国際会議
Masahiko Sakai
IFIP Working Group 1.6: Rewriting
詳細を見る
開催年月日： 2017年9月
記述言語：英語 会議種別：口頭発表（一般）
開催地：Oxford 国名：グレートブリテン・北アイルランド連合王国(英国)
-
Solving QFLIA by combining unit cube test and Smith normal form
Masahiko Sakai
the 46th TRS meeting
詳細を見る
開催年月日： 2017年2月 - 2017年3月
記述言語：英語 会議種別：口頭発表（一般）
開催地：Shinojima, Aichi 国名：日本国
-
Programming in the Esoteric Language Malbolge for Obfuscation 国際会議
Masahiko Sakai
4th Austria--Japan Summer Workshop on Term Rewriting
詳細を見る
開催年月日： 2016年9月
記述言語：英語 会議種別：口頭発表（一般）
開催地：Obergurgl 国名：オーストリア共和国
-
CombSQL: an SQL for Specifying Combinatorial Optimization Problems
SAKAI Masahiko
the 44th TRS meeting
詳細を見る
開催年月日： 2016年2月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
A heuristic procedure for inverse unfold problem
SAKAI Masahiko
the 42nd TRS meeting
詳細を見る
開催年月日： 2015年2月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
A Simple Sufficient Condition for the Completeness of a Heuristic Procedure for Inverse Unfold Problem
Masahiko Sakai, Tatsuki Kato
IPSJ Special Interest Group on Programming
詳細を見る
開催年月日： 2014年11月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
A heuristic procedure for inverse unfold problem
SAKAI Masahiko
the 42nd TRS meeting
詳細を見る
開催年月日： 2014年9月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
On Coding for Problems on Bounded-Integers to Efficient Pseudo-Boolean Constraints - Magic Square as an Example -
SAKAI Masahiko
the 41st TRS meeting
詳細を見る
開催年月日： 2014年9月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
Esoteric Programming Language Malbolge and Its Low-Level Assembler
Masahiko Sakai, Tatsuki Kato
IPSJ Special Interest Group on Programming
詳細を見る
開催年月日： 2014年6月 - 2014年9月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
Size complexity of BDD construction of Pseudo-Boolean constraints in binary/mixed-radix base form
Naoki Nagatsuka, Masahiko Sakai, Harald Zankl, Keiichiro Kusakari
The 28th Annual Conference of the Japan Society of Artifical Intelligence (JSAI 2014), Organized session "Theory, implementation, and application of SAT technology"
詳細を見る
開催年月日： 2014年5月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
On constructing ROBDDs of Pseudo-Boolean constraints in band form and 2-clauses coding
SAKAI Masahiko
the 40th TRS meeting
詳細を見る
開催年月日： 2014年3月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
On Converting Pseudo-Boolean constraints via BDD 国際会議
SAKAI Masahiko
the 39th TRS meeting
詳細を見る
開催年月日： 2013年9月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
項書換え系におけるSAT技術
酒井正彦
2013年度 人工知能学会全国大会(第27回), オーガナイズドセッション「OS-09 SAT技術の理論，実装，応用」
詳細を見る
開催年月日： 2013年6月
記述言語：日本語 会議種別：口頭発表（招待・特別）
開催地：富山市 国名：日本国
-
A CSP solver for bounded-integer linear constraints and its non-linear extension
SAKAI Masahiko
the 38th TRS meeting
詳細を見る
開催年月日： 2013年4月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
On determinazation of conditional rewrite systems
SAKAI Masahiko
the 37th TRS meeting
詳細を見る
開催年月日： 2012年11月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
On Disproving and Postulating for Multi-Context Rewriting Induction
SAKAI Masahiko
the 36th TRS meeting
詳細を見る
開催年月日： 2012年2月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
New Encodings of Pseudo-Boolean Constraints into CNF (by Olivier Bailleux, Yacine Boufkhad, and Olivier Roussel) 国際会議
SAKAI Masahiko
the 35th TRS meeting
詳細を見る
開催年月日： 2011年9月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
CNFs with Elementary Symmetric Clauses and Their SAT Solving 国際会議
Masahiko Sakai, Yohei Umano and Yoshizane Hino
8th Asian Workshop on Foundation of Software (AWFS 2011)
詳細を見る
開催年月日： 2011年5月
記述言語：英語 会議種別：口頭発表（一般）
国名：中華人民共和国
-
Introduction to Esoteric Language Malbolge 国際会議
Japan-Vietnam Workshop on Software Engineering 2010 (JVSE 2010)
詳細を見る
開催年月日： 2010年12月
記述言語：英語 会議種別：口頭発表（招待・特別）
-
例外処理を持つ関数型プログラムの停止性証明法
馬場正貴、酒井正彦、濱口毅、西田直樹、坂部俊樹、草刈圭一朗
第12回プログラミングおよびプログラミング言語ワークショップPPL2010
詳細を見る
開催年月日： 2010年3月
記述言語：日本語 会議種別：ポスター発表
国名：日本国
-
SATソルバを利用したお絵かきロジックの問題作成支援ツール
長坂哲、伊藤寛之、酒井正彦、草刈圭一朗、西田直樹、坂部俊樹
組合せゲーム・パズルミニプロジェクト 第5回ミニ研究集会、東京
詳細を見る
開催年月日： 2010年3月
記述言語：日本語 会議種別：口頭発表（一般）
国名：日本国
-
制約付き等式の定理自動証明器の試作
西田直樹，中林直生、酒井正彦、草刈圭一朗，坂部俊樹
日本ソフトウェア科学会 大会
詳細を見る
開催年月日： 2009年9月
記述言語：日本語 会議種別：ポスター発表
国名：日本国
-
Almost-Non-Overlapping Non-Collapsing Shallow Term Rewriting Systems are Confluent 国際会議
Masahiko Sakai
詳細を見る
開催年月日： 2009年6月
記述言語：英語 会議種別：口頭発表（一般）
-
Decidability of Termination for CS-TRSs with Right-Linear Right-Shallow DPs 国際会議
The 33rd Workshop on Term Rewriting Systems, Tsu
詳細を見る
開催年月日： 2009年2月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
Decidability of termination for TRSs with right-shallow DPs 国際会議
The 31st Workshop on Term Rewriting Systems, Yamanaka
詳細を見る
開催年月日： 2009年2月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
On confluent property of shallow term rewriting systems 国際会議
The 30th Workshop on Term Rewriting Systems, Sapporo
詳細を見る
開催年月日： 2008年8月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
On Decidability of Innermost Terminafor Shallow Term Rewriting Systems
1st Mini-Workshop on Rewriting Techniques, Jaist
詳細を見る
開催年月日： 2008年8月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
Programming in Malbolge 国際会議
The 2nd Austria - Japan Summer Workshop on Term Rewriting, Obergurgl
詳細を見る
開催年月日： 2007年8月
記述言語：英語 会議種別：口頭発表（一般）
-
Straight line programming in Malbolge 国際会議
The 28th Workshop on Term Rewriting Systems, Katayamazu
詳細を見る
開催年月日： 2007年2月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
On decidability of termination 国際会議
The 27th Workshop on Term Rewriting Systems, Katayamazu
詳細を見る
開催年月日： 2006年9月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
On Simulation-Completeness of Unraveling for Conditional Term Rewriting Systems
LA symposium
詳細を見る
開催年月日： 2004年7月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
On Normalizing Strategies of Left-linear Strong-overlay TRSs 国際会議
The 24nd Workshop on Term Rewriting Systems, Matsue
詳細を見る
開催年月日： 2004年4月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
右辺のみに現れる変数を持つ右線形オーバーレイ項書換え系の最左最内ナローイングによる正規形の計算
西田直樹、酒井正彦、坂部俊樹
2003年度夏のLAシンポジウム
詳細を見る
開催年月日： 2003年8月
記述言語：日本語 会議種別：口頭発表（一般）
国名：日本国
-
Decidability of termination for TRSs with right-shallow DPs 国際会議
The 31st Workshop on Term Rewriting Systems, Yamanaka
詳細を見る
開催年月日： 2002年2月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
-
n箇所パターン照合関数のDeforestationに基づく効率化
中村敏広、酒井正彦、坂部俊樹
シンポジウム，情報基礎理論ワークショップ
詳細を見る
開催年月日： 2002年2月
記述言語：日本語 会議種別：口頭発表（一般）
国名：日本国
-
Confluence of Weakly Orthogonal CTRSs with Extra Variables
LA symposium
詳細を見る
開催年月日： 2000年7月
記述言語：英語 会議種別：口頭発表（一般）
国名：日本国
共同研究・競争的資金等の研究課題
共同研究・競争的資金等の研究課題 5
-
制約充足性判定の書換え理論への導入とそのソフトウェア検証への応用
2012年5月 - 2014年3月
日本学術振興会二国間交流事業（共同研究)
詳細を見る
資金種別：競争的資金
-
項書換え系に関するオーストリア日本ワークショップ
2010年8月
日本学術振興会二国間交流事業（セミナー)
詳細を見る
資金種別：競争的資金
-
項書換え理論の関数型言語への応用
2002年4月
日東学術振興財団第19回助成金
詳細を見る
資金種別：競争的資金
-
関数型言語における計算戦略
2000年4月 - 2002年3月
栢森情報科学振興財団研究助成金
詳細を見る
資金種別：競争的資金
-
定理自動証明のためのAC停止性
1998年 - 1999年
財団法人人工知能研究振興財団
詳細を見る
資金種別：競争的資金
科研費
科研費 8
-
形式言語理論に基づく自動採譜 国際共著
研究課題/研究課題番号：20H04302 2020年4月 - 2025年3月
科学研究費補助金 基盤研究(B)
詳細を見る
担当区分：研究代表者 資金種別：競争的資金
配分額：15990000円 （ 直接経費：12300000円 、 間接経費：3690000円 ）
-
データベース上の制約プログラミングのためのSQL言語の拡張とその処理系
研究課題/研究課題番号：17H01721 2017年4月 - 2020年3月
科学研究費補助金 基盤研究(B)
詳細を見る
担当区分：研究代表者
配分額：11050000円 （ 直接経費：8500000円 、 間接経費：2550000円 ）
-
耐改竄性をもつプログラム言語とそのプログラム開発手法の研究
2014年 - 2017年3月
科学研究費補助金 挑戦的萌芽研究
酒井 正彦
詳細を見る
担当区分：研究代表者
-
ソフトウェアプロテクションのための超難読言語Ｍａｌｂｏｌｇｅの研究
2010年 - 2013年3月
科学研究費補助金 挑戦的萌芽研究，課題番号：22650003
酒井 正彦
詳細を見る
担当区分：研究代表者
-
関数型言語の解析・検証・効率的実行のための書換え系理論の研究
2006年4月 - 2010年3月
科学研究費補助金 基盤研究（Ｃ），課題番号：18500011
酒井 正彦
詳細を見る
担当区分：研究代表者
-
関数型言語の解析・検証・効率的実行のための書換え系理論の研究
2003年4月 - 2006年3月
科学研究費補助金 基盤研究（Ｃ），課題番号：15500007
酒井 正彦
詳細を見る
担当区分：研究代表者
-
関数型言語における計算戦略
1999年4月 - 2003年3月
科学研究費補助金 基盤研究(C)(2)・11680352
-
代数的手法に基づくソフトウェアの検証の基礎的研究
1995年 - 1998年
科学研究費補助金 一般研究(C)(2)・07680350
担当経験のある科目 (本学)
担当経験のある科目 (本学) 5
-
プログラム理論特論
2001
-
情報基礎論第1及び演習
1999
-
プログラム理論特論
1999
-
情報基礎論第1及び演習
1998
-
情報基礎論第1及び演習
1997
担当経験のある科目 (本学以外)
担当経験のある科目 (本学以外) 14
-
計算機科学特論Ｉ
2004年4月 - 2005年3月 （高知大学）
-
計算機科学特論Ｉ
2003年4月 - 2004年3月 （高知大学）
-
計算機科学特論Ｉ
2002年4月 - 2003年3月 （高知大学）
-
計算機科学特論Ｉ
2001年4月 - 2002年3月 （高知大学）
-
計算機科学特論Ｉ
2000年4月 - 2001年3月 （高知大学）
-
プログラミングII
2000年4月 - 2001年3月 （愛知県立大学）
-
プログラミングI
2000年4月 - 2001年3月 （愛知県立大学）
-
プログラミングI
1999年4月 - 2000年3月 （愛知県立大学）
-
プログラミングII
1999年4月 - 2000年3月 （愛知県立大学）
-
プログラミングI
1998年4月 - 1999年3月 （愛知県立大学）
-
1993年4月 - 1994年3月 （Toyota National College of Technology）
-
1992年4月 - 1993年3月 （Toyota National College of Technology）
-
1991年4月 - 1992年3月 （Toyota National College of Technology）
-
1990年4月 - 1991年3月 （Toyota National College of Technology）