大学院情報学研究科
情報学部 コンピュータ科学科
2024/10/07 更新
博士(工学) ( 1992年1月 名古屋大学 )
組合せ最適化
項書換え系
音楽情報処理
プログラム意味論
情報通信 / 情報学基礎論 / 項書換え系
情報通信 / ソフトウェア / 組合せ最適化
情報通信 / 知能情報学 / 音楽情報処理
SQLに基づく組み合わせ問題記述法とそのソルバ
Midiからの自動採譜
項書換え系の基礎研究
擬ブール制約問題ソルバ
名古屋大学 大学院情報学研究科 教授
2017年4月 - 現在
国名:日本国
名古屋大学 工学研究科 電気工学,電気工学第二及び電子工学専攻
1986年4月 - 1989年3月
国名: 日本国
名古屋大学 工学研究科 電気工学,電気工学第二及び電子工学専攻
1984年4月 - 1986年3月
国名: 日本国
名古屋大学 工学部 電気学科
1980年4月 - 1984年3月
国名: 日本国
電子情報通信学会
日本ソフトウェア科学会
情報処理学会
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月
第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
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月
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月
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月
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月
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月
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月
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月
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月
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月
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月
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月
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月
基本対象関数に基づく節を持つCNF論理式の充足可能性判定 査読有り
馬野洋平, 酒井正彦, 西田直樹, 坂部俊樹, 草刈圭一朗
電子情報通信学会論文誌 J93-D 巻 ( 1 ) 頁: 1-9 2010年1月
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月
高階書換え系における引数切り落とし法と実効規則
鈴木翔、草刈圭一朗、坂部俊樹、酒井正彦、西田直樹
電子情報通信学会技術研究報告 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月
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月
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月
論理式への変換に基づく魔方陣の発見
伊藤寛之、酒井正彦,草刈圭一朗,坂部俊樹,西田直樹
平成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月
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月
暗号プロトコル記述からカラーペトリネットへの変換による機密性検証
奥谷大介,坂部俊樹,酒井正彦,草刈圭一朗,西田直樹
電子情報通信学会技術報告 105 巻 ( 490 ) 頁: 19-24 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月
重なりを持つ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月
変換と部分評価に基づく非左辺正規なメタ項の停止性証明
"蛸島洋明, 酒井正彦, 坂部俊樹, 西田直樹, 草刈圭一朗"
京都大学数理解析研究所講究録 1426 巻 頁: 113-118 2005年4月
項到達可能性の判定における成長TRSに対する手法と正規化規則による手法の関係
"村田龍彦, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹"
京都大学数理解析研究所講究録 1426 巻 頁: 106-112 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月
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月
左辺が一致するオーバレイ性を持つ左線形TRSの正規化戦略
水野健一、草刈圭一朗、酒井正彦、坂部俊樹
京都大学数理解析研究所講究録 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年度電気関係学会東海支部連合大会講演論文集 頁: 564 2003年10月
メタ項書き換え計算における左辺正規性を持つメタ項の停止性について、
蛸島洋明、酒井正彦、坂部俊樹
平成15年度電気関係学会東海支部連合大会講演論文集 頁: 565 2003年10月
右辺のみに現れる変数を持つ項書換え系の計算モデル 査読有り
西田直樹、酒井正彦、坂部俊樹
コンピュータソフトウェア 20 巻 ( 5 ) 頁: 85-89 2003年9月
限量子付き等式理論の変換に基づく仕様からのプログラム生成、
長島正徳、酒井正彦、坂部俊樹、草刈圭一朗
日本ソフトウェア科学会 第20回大会論文集 頁: 431-435 2003年9月
右辺のみに現れる変数を持つ右線形構成子項書換え系の計算の効率化
西田直樹、酒井正彦、坂部俊樹
日本ソフトウェア科学会 第20回大会論文集 441-445 巻 2003年9月
高階項書換え系の決定可能性問題のためのNk木オートマトンとその性質、
粕谷英人、酒井正彦、阿草清滋
日本ソフトウェア科学会 第20回大会論文集 頁: 436-440 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月
プログラムの設計
坂部俊樹編、分担執筆酒井正彦( 担当: 共著)
オーム社 2000年
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月
小栗 滉介, 酒井正彦, 橋本健二
組合せゲーム・パズル(CGP) プロジェクト, 第18回 研究集会 2024年3月
Ground Canonical Rewrite Systems Revisited 国際共著 国際会議
Aart Middeldorp, Masahiko Sakai, and Sarah Winkler
12th International Workshop on Confluence (IWC 2023) 2023年8月24日
Takeshi Hamaguchi, Masahiko Sakai
Technical report of IEICE, SS group 2023年1月11日
自動演奏への表情付けのための生成音楽理論に基づくフレーズ情報の生成法
後藤 円香, 酒井 正彦, 東条 敏
第135回音楽情報科学研究発表会 2022年9月15日 情報処理学会
番原睦則, 橋本健二, 堀山貴史, 湊真一, 中村駆, 西野正彬, 酒井正彦, 上原隆平, 宇野裕之, 安田宜仁
組合せゲーム・パズル(CGP) プロジェクト, 第16回 研究集会
Equivalence of Context-Free and Regular Languages on Commutative Strings 国際会議
Masahiko Sakai
the 56th TRS meeting 2022年2月24日
命題論理式の全ての投射モデルを表現するBDDの構成法
磯貝孝明, 橋本健二, 酒井正彦
第116回人工知能基本問題研究会 2021年3月22日 人工知能学会
計数セマフォを含むプログラムから論理制約付き項書換え系への変換
小嶋美咲, 西田直樹, 酒井正彦
情報処理学会第83回全国大会 2020年3月20日 情報処理学会
擬ブール制約の導入による組合せ最適化ソルバCombSQL+の高速化
岸潤一郎, 酒井正彦, 西田直樹, 橋本健二
ソフトウェアサイエンス研究会 2021年1月27日 電子情報通信学会
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月
Transformation of SQL-based Combinatorial Optimization Problems into Constraint Problems
2020年9月30日 人工知能学会
On Decision Diagrams
Masahiko Sakai
the 52nd TRS meeting
Rhythm quantization as an efficiently-solvable optimization problem
Masahiko Sakai
the 51st TRS meeting
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)
An extended SQL for combinatorial optimization problems and transformation into constraint problems
Masahiko Sakai
the 49th TRS meeting
Transformation of combinatorial optimization problems written in extended SQL into constraint problems
Genki Sakanashi, Masahiko Sakai
IPSJ-SIGPRO
On Confluence of Innermost Terminating Term Rewriting Systems
Masahiko Sakai
the 47th TRS meeting
On Confluence of Innermost Terminating Term Rewriting Systems 招待有り 国際会議
Masahiko Sakai
IFIP Working Group 1.6: Rewriting
Solving QFLIA by combining unit cube test and Smith normal form
Masahiko Sakai
the 46th TRS meeting
Programming in the Esoteric Language Malbolge for Obfuscation 国際会議
Masahiko Sakai
4th Austria--Japan Summer Workshop on Term Rewriting
CombSQL: an SQL for Specifying Combinatorial Optimization Problems
SAKAI Masahiko
the 44th TRS meeting
A heuristic procedure for inverse unfold problem
SAKAI Masahiko
the 42nd TRS meeting
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
A heuristic procedure for inverse unfold problem
SAKAI Masahiko
the 42nd TRS meeting
On Coding for Problems on Bounded-Integers to Efficient Pseudo-Boolean Constraints - Magic Square as an Example -
SAKAI Masahiko
the 41st TRS meeting
Esoteric Programming Language Malbolge and Its Low-Level Assembler
Masahiko Sakai, Tatsuki Kato
IPSJ Special Interest Group on Programming
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"
On constructing ROBDDs of Pseudo-Boolean constraints in band form and 2-clauses coding
SAKAI Masahiko
the 40th TRS meeting
On Converting Pseudo-Boolean constraints via BDD 国際会議
SAKAI Masahiko
the 39th TRS meeting
項書換え系におけるSAT技術
酒井正彦
2013年度 人工知能学会全国大会(第27回), オーガナイズドセッション「OS-09 SAT技術の理論,実装,応用」
A CSP solver for bounded-integer linear constraints and its non-linear extension
SAKAI Masahiko
the 38th TRS meeting
On determinazation of conditional rewrite systems
SAKAI Masahiko
the 37th TRS meeting
On Disproving and Postulating for Multi-Context Rewriting Induction
SAKAI Masahiko
the 36th TRS meeting
New Encodings of Pseudo-Boolean Constraints into CNF (by Olivier Bailleux, Yacine Boufkhad, and Olivier Roussel) 国際会議
SAKAI Masahiko
the 35th TRS meeting
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)
Introduction to Esoteric Language Malbolge 国際会議
Japan-Vietnam Workshop on Software Engineering 2010 (JVSE 2010)
例外処理を持つ関数型プログラムの停止性証明法
馬場正貴、酒井正彦、濱口毅、西田直樹、坂部俊樹、草刈圭一朗
第12回プログラミングおよびプログラミング言語ワークショップPPL2010
SATソルバを利用したお絵かきロジックの問題作成支援ツール
長坂哲、伊藤寛之、酒井正彦、草刈圭一朗、西田直樹、坂部俊樹
組合せゲーム・パズルミニプロジェクト 第5回ミニ研究集会、東京
制約付き等式の定理自動証明器の試作
西田直樹,中林直生、酒井正彦、草刈圭一朗,坂部俊樹
日本ソフトウェア科学会 大会
Almost-Non-Overlapping Non-Collapsing Shallow Term Rewriting Systems are Confluent 国際会議
Masahiko Sakai
Decidability of Termination for CS-TRSs with Right-Linear Right-Shallow DPs 国際会議
The 33rd Workshop on Term Rewriting Systems, Tsu
Decidability of termination for TRSs with right-shallow DPs 国際会議
The 31st Workshop on Term Rewriting Systems, Yamanaka
On confluent property of shallow term rewriting systems 国際会議
The 30th Workshop on Term Rewriting Systems, Sapporo
On Decidability of Innermost Terminafor Shallow Term Rewriting Systems
1st Mini-Workshop on Rewriting Techniques, Jaist
Programming in Malbolge 国際会議
The 2nd Austria - Japan Summer Workshop on Term Rewriting, Obergurgl
Straight line programming in Malbolge 国際会議
The 28th Workshop on Term Rewriting Systems, Katayamazu
On decidability of termination 国際会議
The 27th Workshop on Term Rewriting Systems, Katayamazu
On Simulation-Completeness of Unraveling for Conditional Term Rewriting Systems
LA symposium
On Normalizing Strategies of Left-linear Strong-overlay TRSs 国際会議
The 24nd Workshop on Term Rewriting Systems, Matsue
右辺のみに現れる変数を持つ右線形オーバーレイ項書換え系の最左最内ナローイングによる正規形の計算
西田直樹、酒井正彦、坂部俊樹
2003年度夏のLAシンポジウム
Decidability of termination for TRSs with right-shallow DPs 国際会議
The 31st Workshop on Term Rewriting Systems, Yamanaka
n箇所パターン照合関数のDeforestationに基づく効率化
中村敏広、酒井正彦、坂部俊樹
シンポジウム,情報基礎理論ワークショップ
Confluence of Weakly Orthogonal CTRSs with Extra Variables
LA symposium
制約充足性判定の書換え理論への導入とそのソフトウェア検証への応用
2012年5月 - 2014年3月
日本学術振興会二国間交流事業(共同研究)
資金種別:競争的資金
項書換え系に関するオーストリア日本ワークショップ
2010年8月
日本学術振興会二国間交流事業(セミナー)
資金種別:競争的資金
項書換え理論の関数型言語への応用
2002年4月
日東学術振興財団第19回助成金
資金種別:競争的資金
関数型言語における計算戦略
2000年4月 - 2002年3月
栢森情報科学振興財団研究助成金
資金種別:競争的資金
定理自動証明のためのAC停止性
1998年 - 1999年
財団法人人工知能研究振興財団
資金種別:競争的資金
形式言語理論に基づく自動採譜 国際共著
研究課題/研究課題番号:20H04302 2020年4月 - 2025年3月
科学研究費補助金 基盤研究(B)
担当区分:研究代表者 資金種別:競争的資金
配分額:15990000円 ( 直接経費:12300000円 、 間接経費:3690000円 )
データベース上の制約プログラミングのためのSQL言語の拡張とその処理系
研究課題/研究課題番号:17H01721 2017年4月 - 2020年3月
科学研究費補助金 基盤研究(B)
担当区分:研究代表者
配分額:11050000円 ( 直接経費:8500000円 、 間接経費:2550000円 )
耐改竄性をもつプログラム言語とそのプログラム開発手法の研究
2014年 - 2017年3月
科学研究費補助金 挑戦的萌芽研究
酒井 正彦
担当区分:研究代表者
ソフトウェアプロテクションのための超難読言語Malbolgeの研究
2010年 - 2013年3月
科学研究費補助金 挑戦的萌芽研究,課題番号:22650003
酒井 正彦
担当区分:研究代表者
関数型言語の解析・検証・効率的実行のための書換え系理論の研究
2006年4月 - 2010年3月
科学研究費補助金 基盤研究(C),課題番号:18500011
酒井 正彦
担当区分:研究代表者
関数型言語の解析・検証・効率的実行のための書換え系理論の研究
2003年4月 - 2006年3月
科学研究費補助金 基盤研究(C),課題番号:15500007
酒井 正彦
担当区分:研究代表者
関数型言語における計算戦略
1999年4月 - 2003年3月
科学研究費補助金 基盤研究(C)(2)・11680352
代数的手法に基づくソフトウェアの検証の基礎的研究
1995年 - 1998年
科学研究費補助金 一般研究(C)(2)・07680350
プログラム理論特論
2001
情報基礎論第1及び演習
1999
プログラム理論特論
1999
情報基礎論第1及び演習
1998
情報基礎論第1及び演習
1997
計算機科学特論I
2004年4月 - 2005年3月 (高知大学)
計算機科学特論I
2003年4月 - 2004年3月 (高知大学)
計算機科学特論I
2002年4月 - 2003年3月 (高知大学)
計算機科学特論I
2001年4月 - 2002年3月 (高知大学)
計算機科学特論I
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)