Updated on 2024/10/07
博士(工学) （ 1992.1 名古屋大学 ）
Combinatorial optimization
Term rewriting system
音楽情報処理
Semantics of programs
Informatics / Theory of informatics / Term rewriting systems
Informatics / Software / Combinatorial optimization
Informatics / Intelligent informatics / 音楽情報処理
Mechanical proof of security
Midiからの自動採譜
項書換え系の基礎研究
Psudo-Boolean constraint solver
Nagoya University Professor
2017.4
Country：Japan
Nagoya University Graduate School, Division of Engineering
1986.4 - 1989.3
Country： Japan
Nagoya University Graduate School, Division of Engineering
1984.4 - 1986.3
Country： Japan
Nagoya University Faculty of Engineering
1980.4 - 1984.3
Country： Japan
電子情報通信学会
日本ソフトウェア科学会
情報処理学会
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
Best Paper Award of IEICE
2011.5 IEICE
Best Paper Award of IEICE
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 Reviewed International coauthorship
Florent Jacquemard, Masahiko Sakai, Yosuke Amagasu
Proceedings of the International Conference on Technologies for Music Notation and Representation (TENOR 2024) page： 98 - 108 2024.4
演奏MIDIのリズム量子化のためのトークン化の提案
天春 陽介, 酒井 正彦
情報処理学会技術報告 SIGMUS 2024.3
Automatic Phrasing System for Expressive Performance Based on The Generative Theory of Tonal Music Reviewed
Madoka Goto, Masahiko Sakai, Satoshi Tojo
The 16th International Symposium on Computer Music Multidisciplinary Research page： 536 - 546 2023.9
8+8=4: Formalizing Time Units to Handle Symbolic Music Durations Reviewed International coauthorship
Emmanouil Karystinaios, Francesco Foscarin, Florent Jacquemard, Masahiko Sakai, Satoshi Tojo and Gerhard Widmer
The 16th International Symposium on Computer Music Multidisciplinary Research page： 536 - 546 2023.9
Ground Canonical Rewrite Systems Revisited Reviewed International coauthorship
Aart Middeldorp, Masahiko Sakai, Sarah Winkler
12th International Workshop on Confluence page： 44 - 48 2023.8
SQL 型制約プログラミングシステム CombSQL+ の複数制約ソルバー連携
小菅 脩司、酒井 正彦、番原 睦則
人工知能学会研究会資料 Vol. 125 page： 54 - 59 2023.8
レプ・タイルの定式化を用いた各種ソルバの性能比較
番原 睦則, 橋本 健二, 堀山 貴史, 湊 真一, 中村 駆, 西野 正彬, 酒井 正彦, 上原 隆平, 宇野 裕之, 安田 宜仁
人工知能学会研究会資料 人工知能基本問題研究会 Vol. 119 ( 0 ) page： 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
Describing Car Sequencing Problem by SQL-based solver CombSQL+
INOUE Kazuya, KISHI Junichiro, SAKAI Masahiko
Proceedings of the Annual Conference of JSAI Vol. JSAI2021 ( 0 ) page： 2E4OS13c01 - 2E4OS13c01 2021.6
Transformation of SQL-based Combinatorial Optimization Problems into Constraint Problems
Genki Sakanashi, Masahiko Sakai
SIG-FPAI-112 Vol. 112 ( 4 ) page： 6pages 2020.3
Conditions for Confluence of Innermost Terminating Term Rewriting Systems Reviewed
Sayaka Ishizuki, Masahiko Sakai, and Michio Oyamaguchi
Applicable Algebra in Engineering, Communication and Computing Vol. 30 ( 4 ) page： 349-360 2019.8
A Parse-based Framework for Coupled Rhythm Quantization and Score Structuring Reviewed
Francesco Foscarin, Florent Jacquemard, Philippe Rigaux, and Masahido Sakai
Lecture Notes in Artificial Intelligence Vol. 11502 page： 248-260 2019.6
Transformation of Combinatorial Optimization Problems Written in Extended SQL into Constraint Problems Reviewed
Genki Sakanashi and Masahiko Sakai
Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming (PPDP 2018) page： 19:1-19:13 2018.9
Reduced dependency spaces for existential parameterised Boolean equation system Reviewed
Yutaro Nagae, Masahiko Sakai
Electronic Proceedins in Theoretical Computer Science (EPTCS) Vol. 265 page： 67-81 2018.1
Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers Reviewed
Tomohiro Sasano, Naoki Nishida, Masahiko Sakai, and Tomoya Ueyama
Electronic Proceedins in Theoretical Computer Science (EPTCS) Vol. 265 page： 82-97 2018.1
Generating Equivalent Rhythmic Notations Based on Rhythm Tree Languages Reviewed
Florent Jacquemard, Adrien Ycart, and Masahiko Sakai
Proceedings of the International Conference on Technologies for Music Notation and Representation page： 145-153 2017.5
Sound Structure-Preserving Transformation for Weakly-Left-Linear Deterministic Conditional Term Rewriting Systems Reviewed
Ryota Nakayama, Naoki Nishida and Masahiko Sakai
Electronic Proceedins in Theoretical Computer Science Vol. 235 page： 62-77 2017.1
An extension of proof graphs for disjunctive parameterised Boolean equation systems Reviewed
Yutaro Nagae, and Masahiko Sakai and Hiroyuki Seki
Electronic Proceedins in Theoretical Computer Science Vol. 235 page： 46-61 2017.1
Sound Structure-Preserving Transformation for Ultra-Weakly-Left-Linear Determini stic Conditional Term Rewriting Systems Reviewed
Ryota Nakayama, Naoki Nishida, Masahiko Sakai
Informal Proceedings of the 3rd International Workshop on Rewriting Techniques f or Program Transformations and Evaluation (WPTE 2016) page： 61-75 2016.9
An extension of proof graphs for disjunctive parameterised Boolean equation systems Reviewed
Yutaro Nagae, Masahiko Sakai
Informal Proceedings of the 3rd International Workshop on Rewriting Techniques f or Program Transformations and Evaluation (WPTE 2016) page： 3-14 2016.9
Conditions for confluence of innermost terminating term rewriting systems Reviewed
Sayaka Ishizuki, Masahiko Sakai, Michio Oyamaguchi
Proceedings of the 5th International Workshop on Confluence (IWC 2016) page： 65-69 2016.9
Non-E-overlapping, weakly shallow, and non-collapsing TRSs are confluent Reviewed
Masahiko Sakai, Michio Oyamaguchi, Mizuhito Ogawa
Lecture Notes in Computer Science (CADE 2015) Vol. 9195 page： 111-126 2015.8
Term Rewriting with Prefix Context Constraints and Regularity Preservation and Bottom-Up Strategies Reviewed
Yoshiharu Kojima, Masahiko Sakai, Florent Jacquemard
Lecture Notes in Computer Science (CADE 2015) Vol. 9195 page： 137-151 2015.8
Construction of an ROBDD for a PB-constraint in band form and related techniques for PB-solvers Reviewed
Masahiko Sakai, Hidetomo Nabeshima
IEICE Transaction on Information and Systems Vol. E98-D ( 6 ) page： 1121-1127 2015.6
Towards an Equational Theory of Rhythm Notation Reviewed
Pierre Donat-Bouillud, Florent Jacquemard, and Masahiko Sakai
Proc. of The Music Encoding Conference 2015 page： 2 pages 2015.5
Non-E-overlapping and weakly shallow TRSs are confluent Reviewed
Masahiko Sakai, Michio Oyamaguchi, Mizuhito Ogawa
Proceedings of the 3rd International Workshop on Confluence (IWC 2014) page： 34-38 2014.7
Inverse Unfold Problem and Its Heuristic Solving Reviewed
Masanori Nagashima, Tomofumi Kato, Masahiko Sakai and Naoki Nishida
OASIcs Vol. 40 page： 27-38 2014.7
On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms Reviewed
Naoki Nishida, Masahiko Sakai, Yasuhiro Nakano
Electronic Proceedings in Theoretical Computer Science Vol. 134 page： 1-10 2013.10
Improving Determinization of Grammar Programs for Program Inversion Reviewed
Minami Niwa, Naoki Nishida, and Masahiko Sakai
Lecture Notes in Computer Science Vol. 7844 page： 137-154 2013.4
Determinization of conditional term rewriting systems Invited Reviewed
Masanori Nagashima, Masahiko Sakai, Toshiki Sakabe
Theoretical Computer Science Vol. 464 page： 72-89 2012.12
Extending Matching Operation in Grammar Program for Program Inversion Reviewed
Minami Niwa, Naoki Nishida, and Masahiko Sakai
Proceedings of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2012) page： 130-139 2012.9
Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity Reviewed
Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe
Logical Methods in Computer Science Vol. 8 ( 3-4 ) page： 1-49 2012.8
On determinazation of conditional term rewriting systems Reviewed
Masahiko Sakai
Proc. of 9th Asian Workshop on Foundation of Software (AWFS 2012) page： 18-19 2012.6
Constrained Tree Automata and their Closure Properties Reviewed
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) page： 24-34 2012.6
A Sound Type System for Typing Runtime Errors Reviewed
YAMADA Akihisa, KUSAKARI Keiichirou, SAKABE Toshiki, SAKAI Masahiko, NISHIDA Naoki
IPSJ Transactions on Programming page： to appear 2012.3
Controlled Term Rewriting Reviewed
Florent Jacquemard, KOJIMA Yoshiharu, and SAKAI Masahiko
Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FroCos 2011), LNCS Vol. 6989 page： 179-194 2011.10
Decidability of Reachability for Right-Shallow Context-Sensitive Term Rewriting Systems Reviewed
KOJIMA Yoshiharu, SAKAI Masahiko, NISHIDA Naoki, KUSAKARI Keiichirou, SAKABE Toshiki
IPSJ Transactions on Programming Vol. 4 ( 4 ) page： 12-35 2011.9
Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity Reviewed
NISHIDA Naoki, SAKAI Masahiko, SAKABE Toshiki
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), LIPIcs Vol. 10 page： 267-282 2011.5
例外処理を持つ関数型プログラムの停止性・非停止性証明法 Reviewed
濱口 毅, 酒井正彦, 馬場正貴, 阿草清滋
Vol. 4 ( 2 ) page： 1-19 2011.3
Lemma Generation Method in Rewriting Induction for Constrained Term Rewriting Systems Reviewed
Naoki NAKABAYASHI, Naoki NISHIDA, Keiichirou KUSAKARI, Toshiki SAKABE and Masahiko SAKAI
Computer Software Vol. 28 ( 1 ) page： 173-189 2011.2
順方向ナローイングに基づく右線形右シャロー項書換え系の非停止性証明について
服部達哉、酒井正彦、西田直樹、草刈圭一朗、坂部俊樹
電子情報通信学会技術研究報告 Vol. 110 ( 336 ) page： 31-36 2010.12
等式理論を法とするDPLL遷移系について
馬場達也、坂部俊樹、西田直樹、草刈圭一朗、酒井正彦
電子情報通信学会技術研究報告 Vol. 110 ( 227 ) page： 49-54 2010.10
難解言語Malbolgeのチューリング完全性について
長坂 哲、酒井正彦、坂部俊樹、草刈圭一朗、西田直樹
電子情報通信学会技術研究報告 Vol. 110 ( 227 ) page： 55-60 2010.10
Weakly-non-overlapping non-collapsing shallow term rewriting systems are confluent Reviewed
Masahiko Sakai, Mizuhito Ogawa
Information Processing Letters Vol. 110 ( 18-19 ) page： 795-844 2010.9
等式論理を法とする抽象DPLLアルゴリズムの提案
馬場達也、坂部俊樹、酒井正彦、草刈圭一朗、西田直樹
平成22年度電気関係学会東海支部連合大会講演論文集 page： D3-4 2010.8
制約付き項書換え系における関数の効率的な等価性検証
高桑一也、西田直樹、酒井正彦、坂部俊樹、草刈圭一朗
平成22年度電気関係学会東海支部連合大会講演論文集 page： D3-6 2010.8
2カウンタ法に基づく基本対称節を持つCNF論理式のSATソルバ
日野善信、酒井正彦、草刈圭一朗、坂部俊樹、西田直樹
平成22年度電気関係学会東海支部連合大会講演論文集 page： D3-5 2010.8
On Disproving Termiation of Constrained Term Rewriting Systems Reviewed
Naoki Nishida, Masahiko Sakai, Tatsuya Hattori
Proc. of Ninth International Workshop on Termination, (WST2010) page： 5 pages 2010.7
Decidability of Termination and Innermost Termination for Term Rewriting Systems with Right-Shallow Dependency Pairs Reviewed
UCHIYAMA Keita, SAKAI Masahiko, SAKABE Toshiki
IEICE Transaction on Information and Systems Vol. E93-D ( 5 ) page： 953-962 2010.5
Proving Injectivity of Functions via Program Inversion in Term Rewriting. Reviewed
Naoki Nishida and Masahiko Sakai
Proceedings of the 10th International Symposium on Functional and Logic Programming (FLOPS 2010),Lecture Notes in Computer Science Vol. 6009 page： 288-303 2010.4
Solving Satisfiability of CNF Formulas with Clauses based on Elementary Symmetric Functions Reviewed
Vol. J93-D ( 1 ) page： 1-9 2010.1
Decidability of Termination and Innermost Termination for Term Rewriting Systems with Right-Shallow Dependency Pairs Reviewed
Keita Uchiyama, Masahiko Sakai, Toshiki Sakabe
IEICE Trans. on Information and Systems Vol. E93-D ( 5 ) page： 953-962 2010.1
高階書換え系における引数切り落とし法と実効規則
鈴木翔、草刈圭一朗、坂部俊樹、酒井正彦、西田直樹
電子情報通信学会技術研究報告 Vol. 109 ( 343 ) page： 25-30 2009.12
条件付き等式の変換に基づくプログラム生成
長島正憲，酒井正彦，坂部俊樹，西田直樹，草刈圭一朗
電子情報通信学会技術研究報告 Vol. 109 ( 343 ) page： 37-42 2009.12
右線形右シャローな項書換え系における文脈依存停止性の決定可能性について
御宿義勝、酒井正彦、坂部俊樹、草刈圭一朗、西田直樹
電子情報通信学会技術研究報告 Vol. 109 ( 343 ) page： 31-36 2009.12
Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems Reviewed
Yasuo Isogai, Keiichirou Kusakari, Masahiko Sakai, Frederic Blanqui
IEICE Trans. on Information and Systems Vol. E92-D ( 10 ) page： 235-247 2009.10
制約付き項書換え系の書換え帰納法における補題等式の自動生成法
中林直生，西田直樹，草刈圭一朗，坂部俊樹，酒井正彦
日本ソフトウェア科学会 第26回大会論文集 Vol. 7B-12 page： 1-14 2009.9
Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems Reviewed
Yoshiharu Kojima, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, Toshiki Sakabe
IPSJ Transactions of Programming Vol. 2 ( 3 ) page： 20-32 2009.7
制約付き項書換え系における書換え帰納法 Reviewed
坂田 翼, 西田 直樹, 酒井 正彦, 草刈 圭一朗, 坂部 俊樹
情報処理学会論文誌プログラミング Vol. 2 ( 2 ) page： 80-96 2009.3
Recognizability of Redexes for Higher-Order Rewrite Systems Reviewed
Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa
IPSJ Transactions of Programming Vol. 2 ( 2 ) page： 166-175 2009.3
Head-Needed Strategy of Higher-Order Rewrite Systems and Its Decidable Classes Reviewed
Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa
IPSJ Transactions of Programming Vol. 2 ( 2 ) page： 144-165 2009.3
Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques Reviewed
Keiichirou Kusakari, Masahiko Sakai
IEICE Trans. on Information and Systems Vol. E92-D ( 2 ) page： 235-247 2009.2
制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み Reviewed
古市 祐樹, 西田 直樹, 酒井 正彦, 草刈 圭一朗, 坂部 俊樹
情報処理学会論文誌プログラミング Vol. 1 ( 2 ) page： 100-121 2008.9
*Innermost Reachability and Context Sensitive Reachability Properties are Decidable for Linear Right-Shallow Term Rewriting Systems Reviewed
Yoshiharu Kojima, Masahiko Sakai
Proc. of 19th Int'l Conference on Rewriting Techniqes and Applications, Hagenberg RTA2008, LNCS Vol. 5117 page： 187-201 2008.7
Completion as Post-Process in Program Inversion of Injective Functions Reviewed
Naoki Nishida, Masahiko Sakai
"Proc. of 8th International Workshop on Reduction Strategies in Rewriting and Programming, Hagenberg (WRS2008)" page： 61-75 2008.7
Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems Reviewed
Keita Uchiyama, Masahiko Sakai and Toshiki Sakabe
Electronic Notes in Theoretical Computer Science Vol. 204 ( 4 ) page： 21-34 2008.4
*Undecidable Properties on Length-Two String Rewriting Systems Reviewed
Masahiko Sakai and Wang Yi
Electronic Notes in Theoretical Computer Science Vol. 204 ( 4 ) page： 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 Vol. 107 ( 505 ) page： 7-12 2008.3
A Type System for Analyzing Secure Information Flow in Object-Oriented Programs with Exception Handling Reviewed
IEICE Trans. on Information and Systems Vol. J91-D ( 3 ) page： 757-770 2008.3
等式を規則化する変換の停止条件
水野清貴，西田直樹，坂部俊樹、酒井正彦，草刈圭一朗
電子情報通信学会技術研究報告 Vol. 107 ( 505 ) page： 25-30 2008.3
Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques
"Keiichirou Kusakari, Masahiko Sakai"
IEICE Technical Report Vol. 107 ( 505 ) page： 19-24 2008.3
プログラム生成系GeneSysにおける等式仕様への否定の導入
近藤悟、酒井正彦、坂部俊樹、草刈圭一朗、西田直樹
電子情報通信学会技術研究報告 Vol. 107 ( 392 ) page： 43-48 2007.12
対話型埋込みによる数独問題の設計ツール
馬野洋平、酒井正彦、西田直樹、坂部俊樹、草刈圭一朗
電子情報通信学会技術研究報告 Vol. 107 ( 392 ) page： 73-78 2007.12
導出木からのループ検出による論理プログラムの非停止性証明法
水谷知博、西田直樹、酒井正彦、坂部俊樹、草刈圭一朗、
電子情報通信学会技術研究報告 Vol. 107 ( 275 ) page： 1-6 2007.10
*Enhancing Dependency Pair Method using Strong Computability in Simply-Typed Term Rewriting Reviewed
Keiichirou Kusakari, Masahiko Sakai
Applicable Algebra in Engineering, Communication and Computing Vol. 18 ( 5 ) page： 407-431 2007.10
論理式への変換に基づく魔方陣の発見
伊藤寛之、酒井正彦，草刈圭一朗，坂部俊樹，西田直樹
平成19年度電気関係学会東海支部連合大会講演論文集 page： O-012 2007.9
左線形は定向条件付き項書換え系における到達可能な項集合の近似集合を認識する木オートマトン
村田俊樹、西田直樹、酒井正彦、坂部俊樹、草刈圭一朗
電子情報通信学会技術研究報告 Vol. 107 ( 176 ) page： 1-6 2007.8
振舞等価性の証明のための等式付き書換えに基づく潜在帰納法
笹田悠司、酒井正彦、西田直樹、坂部俊樹、草刈圭一朗
電子情報通信学会技術研究報告 Vol. 107 ( 176 ) page： 7-12 2007.8
Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems Reviewed
"Keita Uchiyama, Masahiko Sakai and Toshiki Sakabe"
"Proc. of 7th International Workshop on Reduction Strategies in Rewriting and Programming, Paris (WRS2007)" page： 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"
Vol. 107 ( 99 ) page： 17-22 2007.6
二階の書換え系における引数切り落とし法
磯谷泰巨、草刈圭一朗、酒井正彦、坂部俊樹、西田直樹
電子情報通信学会技術研究報告 Vol. 107 ( 99 ) page： 23-28 2007.6
Convergent Term Rewriting Systems for Inverse Computation of Injective Functions Reviewed
"WaNaoki Nishida, Masahiko Sakai, and Terutoshi Kato"
"Proc. of Ninth International Workshop on Termination, Paris (WST2007)" page： 77-81 2007.6
Undecidable Properties on Length-Two String Rewriting Systems Reviewed
Masahiko Sakai and Wang Yi
"Proc. of 7th International Workshop on Reduction Strategies in Rewriting and Programming, Paris (WRS2007)" page： 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" Vol. 1554 page： 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" Vol. 1554 page： 171-177 2007.5
Usable Rules and Labeling Producfor Dependency Pair Method in Simply-Typed Term Rewriting Systemst-Typed Terms Reviewed
"Takahiro Sakurai, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida"
IEICE Trans. on Information and Systems Vol. J90-D ( 4 ) page： 978-989 2007.4
単純型項書換え系における定理自動証明系HOPSYS
蒲田 明憲，草刈 圭一朗，西田 直樹，酒井 正彦，坂部 俊樹
電子情報通信学会技術研究報告 Vol. 106 ( 424 ) page： 7-12 2006.12
手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み
古市祐樹，西田 直樹，酒井 正彦，草刈 圭一朗，坂部 俊樹
電子情報通信学会技術研究報告 Vol. 106 ( 324 ) page： 7-12 2006.10
GeneSysによるプログラム生成例とIntroduction規則の追加
近藤 悟，酒井 正彦，西田 直樹，坂部 俊樹，草刈 圭一朗
電子情報通信学会技術研究報告 Vol. 106 ( 324 ) page： 37-42 2006.10
例外処理付きオブジェクト指向言語における情報流の安全性解析
黒川 翔，桑原寛明，山本晋一郎，坂部俊樹，酒井正彦，草刈圭一朗，西田直樹
電子情報通信学会技術研究報告 Vol. 106 ( 324 ) page： 13-18 2006.10
高階関数機能を持つ項書換え系のコンパイル
笹田悠司，酒井正彦，坂部俊樹，草刈圭一朗，西田直樹
平成18年度電気関係学会東海支部連合大会講演論文集 page： O-437 2006.9
所属制約を持つ条件付き項書換え系の紐解き変換
村田俊樹，西田直樹，酒井正彦，坂部俊樹，草刈圭一朗
平成18年度電気関係学会東海支部連合大会講演論文集 page： O-438 2006.9
*Decidability of Termination Left-Linear Shallow TRSs and Related Systems for Semi-Constructor TRSs Reviewed
Wang Yi and Masahiko Sakai
Proc. of 17th Int'l Conference on Rewriting Techniqes and Applications, Seattle RTA2006, LNCS Vol. 4098 page： 343-356 2006.8
Transformation for Refining Unraveled Conditional Term Rewriting Systems Reviewed
"Naoki Nishida, Tomohiro Mizutani, and Masahiko Sakai"
"Proc. of 6th International Workshop on Reduction Strategies in Rewriting and Programming, Seattle (WRS2006)" page： 34-48 2006.8
On Non-looping Term Rewriting Reviewed
Wang Yi and Masahiko Sakai
"Proc. of Eighth International Workshop on Termination, Seattle (WST2006)" page： 17-21 2006.8
等式付き書換え系の等式数を削減する変換
三浦浩一，西田直樹，酒井正彦，坂部俊樹，草刈圭一朗
電子情報通信学会技術研究報告 Vol. 106 ( 120 ) page： 7-12 2006.6
単純型項書換え系上の依存対法における実行規則と直積型項へのラベル付け
櫻井敬大，草刈圭一朗，酒井正彦，坂部俊樹，西田直樹
電子情報通信学会技術研究報告 Vol. 106 ( 120 ) page： 13-18 2006.6
紐解かれた項書換え系の文脈依存条件の除去のための変換
"水谷知博，西田直樹, 酒井正彦,草刈圭一朗, 坂部俊樹"
京都大学数理解析研究所講究録 Vol. 1489 page： 195-201 2006.5
強計算依存対法による高階書換え系の停止性証明
磯谷泰巨，草刈圭一朗，酒井正彦，坂部俊樹，西田直樹
電子情報通信学会技術研究報告 Vol. 106 ( 15 ) page： 31-36 2006.4
項正規表現に基づくSpi計算の機密性検証
"田代善彦, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹"
電子情報通信学会技術研究報告 Vol. 105 ( 596 ) page： 35-40 2006.2
関数プログラムの停止性証明に関する辞書式経路順序
"星野由美, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹"
電子情報通信学会技術研究報告 Vol. 105 ( 597 ) page： 13-18 2006.2
Primitive Indeuctive Theorems Bridge Implicit Induction methods and Inductive Theorems in Higher-Order Rewriting Reviewed
"Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe"
IEICE Trans. on Information and Systems Vol. E88-D ( 12 ) page： 2715-2726 2005.12
暗号プロトコル記述からカラーペトリネットへの変換による機密性検証
奥谷大介，坂部俊樹，酒井正彦，草刈圭一朗，西田直樹
電子情報通信学会技術報告 Vol. 105 ( 490 ) page： 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 Vol. 105 ( 499 ) page： 9-13 2005.12
分散JoinJAVAプログラムの通信エラーに対する型判定システム
佐伯昌樹，坂部俊樹，酒井正彦，草刈圭一朗，西田直樹
電子情報通信学会技術報告 Vol. 105 ( 491 ) page： 25-30 2005.12
強計算性による単純型項書換え系の依存対法の改良
Vol. 105 ( 491 ) page： 13-18 2005.12
重なりを持つTRSにおける最外戦略の完全性について
"岩田篤史，酒井正彦，西田直樹，草刈圭一朗, 西田直樹"
電子情報通信学会技術報告 SS2005-46 Vol. 105 ( 331 ) page： 39-44 2005.10
カラーペトリネットを用いた暗号プロトコルの安全性検証
奥谷大介、坂部俊樹、酒井正彦、草刈圭一朗、西田直樹
平成17年度電気関係学会東海支部連合大会講演論文集 page： O-198 2005.9
分散JoinJAVAプログラムの正常実行判定のための型システム
佐伯昌樹、坂部俊樹、酒井正彦、草刈圭一朗、西田直樹
平成17年度電気関係学会東海支部連合大会講演論文集 page： O-306 2005.9
Proving Sufficient Completeness of Functional Programs based on Recursive Structure Analysis and Strong Computability Reviewed
Information Technology Letters Vol. LA-001 page： 1-4 2005.9
Generation of Inverse Computation Programs for Constructor Term Rewriting Systems Reviewed
"Naoki Nishida, Masahiko Sakai, Toshiki Sakabe"
Vol. J88-D-I ( 8 ) page： 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" Vol. 105 ( 228 ) page： 13-18 2005.8
難読プログラミング言語Malbolgeにおけるプログラム構成手法
"飯澤 恒, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹"
電子情報通信学会技術報告 Vol. SS2005-22 page： 25-30 2005.6
弱最内戦略を完全にする項書換え系の等価変換
"岡本晃治, 酒井正彦, 西田直樹, 草刈圭一朗"
京都大学数理解析研究所講究録 Vol. 1426 page： 119-125 2005.4
変換と部分評価に基づく非左辺正規なメタ項の停止性証明
"蛸島洋明, 酒井正彦, 坂部俊樹, 西田直樹, 草刈圭一朗"
京都大学数理解析研究所講究録 Vol. 1426 page： 113-118 2005.4
項到達可能性の判定における成長TRSに対する手法と正規化規則による手法の関係
"村田龍彦, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹"
京都大学数理解析研究所講究録 Vol. 1426 page： 106-112 2005.4
Partial Inversion of Constructor Term Rewriting Systems Reviewed
"Naoki Nishida, Masahiko Sakai, Toshiki Sakabe"
"Proc. of 16th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science" Vol. 3647 page： 264-278 2005.4
配列を扱う非線形先頭再帰プログラムからの再帰除去
"高須洋平, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹"
京都大学数理解析研究所講究録 Vol. 1426 page： 39-44 2005.4
On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems Reviewed
"Masahiko Sakai, Keiichirou Kusakari"
IEICE Trans. on Information and Systems Vol. E88-D ( 3 ) page： 583-593 2005.3
項の全正規形を探索するためのTRSコンパイラ
岩田篤史、草刈圭一朗、酒井正彦、坂部俊樹
平成16年度電気関係学会東海支部連合大会講演論文集 page： 363 2004.9
項書換え系と木オートマトンを用いた共通鍵方式暗号プロトコルの検証法
奥谷大介、坂部俊樹、酒井正彦
平成16年度電気関係学会東海支部連合大会講演論文集 page： 352 2004.9
高階書換え系の決定可能な計算戦略について
粕谷英人、酒井正彦、阿草清滋
電子情報通信学会技術報告 Vol. SS2004-6 page： 1-6 2004.8
On Simulation-Completeness of Unraveling for Conditional Term Rewriting Systems
"Naoki Nishida, Masahiko Sakai, Toshiki Sakabe"
Technical Report of IEICE Vol. SS2004-6 page： 25-30 2004.8
On Simulation-Completeness of Unraveling for Conditional Term Rewriting Systems
Naoki Nishida, Masahiko Sakai, Toshiki Sakabe
LA symposium page： 7.1-7.6 2004.7
Program Generation by Transformation from Quantified Equational Specifications Reviewed
Vol. 21 ( 4 ) page： 49-54 2004.7
左辺が一致するオーバレイ性を持つ左線形ＴＲＳの正規化戦略
水野健一、草刈圭一朗、酒井正彦、坂部俊樹
京都大学数理解析研究所講究録 Vol. 1375 page： 247-252 2004.5
Improving Efficiency of Linear Constructor Term Rewriting Systems with Extra Variables Reviewed
Vol. 21 ( 3 ) page： 40-47 2004.5
非完全な仕様における振舞等価性の自動証明法
山本友和、草刈圭一朗、酒井正彦、坂部俊樹
電子情報通信学会技術報告 Vol. COMP2003 ( 66 ) page： 29-36 2003.12
Characterizing Inductive Theorems by Extensional Initial Models in a Higher-Order Equational Logic
"Keiichiro Kusakari, Masahiko Sakai, Toshiki Sakabe"
Vol. 46 ( 9 ) 2003.10
最内書換えに基づく項書換え系の完全な書換え戦略
岡本晃治、酒井正彦、坂部俊樹
平成15年度電気関係学会東海支部連合大会講演論文集 page： 564 2003.10
メタ項書き換え計算における左辺正規性を持つメタ項の停止性について、
蛸島洋明、酒井正彦、坂部俊樹
平成15年度電気関係学会東海支部連合大会講演論文集 page： 565 2003.10
A Computation Model of Term Rewriing Systems Reviewed
Vol. 20 ( 5 ) page： 85-89 2003.9
限量子付き等式理論の変換に基づく仕様からのプログラム生成、
長島正徳、酒井正彦、坂部俊樹、草刈圭一朗
日本ソフトウェア科学会 第20回大会論文集 page： 431-435 2003.9
右辺のみに現れる変数を持つ右線形構成子項書換え系の計算の効率化
西田直樹、酒井正彦、坂部俊樹
日本ソフトウェア科学会 第20回大会論文集 Vol. 441-445 2003.9
高階項書換え系の決定可能性問題のためのNk木オートマトンとその性質、
粕谷英人、酒井正彦、阿草清滋
日本ソフトウェア科学会 第20回大会論文集 page： 436-440 2003.9
右辺のみに現れる変数を持つ右線形オーバーレイ項書換え系の最左最内ナローイングによる正規形の計算
西田直樹、酒井正彦、坂部俊樹
2003年度夏のLAシンポジウム page： 24.1-24.6 2003.8
右辺のみに現れる変数を持つ右線形オーバーレイ項書換え系の最左最内ナローイングによる正規形の計算
西田直樹、酒井正彦、坂部俊樹
2003年度夏のLAシンポジウム page： 24.1-24.6 2003.8
Innermost Reductions Find All Normal Forms on Right-Linear Terminating Overlay TRSs Reviewed
"Masahiko Sakai, Kouji Okamoto, Toshiki Sakabe"
Proc. of 3rd Int'l Workshop on Reduction Strategies in Rewriting and Programming Vol. WRS'03 page： 79-88 2003.6
Narrowing-based Simulation of Term Rewriting Systems with Extra Variables and its Termination Proof Reviewed
"Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe"
Proc. of 12th Int'l Workshop on Functional and (Constraint) Logic Programming Vol. WFLP'03 page： 198-211 2003.6
Narrowing-based Effective Rewriting and its Termination for Term Rewriting Systems with Extra Variables
Vol. 1325 page： 238-243 2003.5
Typing Exception in an Object Oriented Calculus with Recoursive Type
Vol. 1325 page： 104-109 2003.5
オブジェクト指向計算モデルにおける例外処理機能の型付 Reviewed
堀江美保子、酒井正彦、坂部俊樹
コンピュータソフトウェア Vol. 20 ( 2 ) page： 54-58 2003.3
Descendants and Head Normalization of Higher-Order Rewrite Systems Reviewed
"Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa"
Lecture Notes in Computer Science Vol. 2441 2002.9
On Proving Termination of Higher-Order Rewrite Systems by Dependency Pair technique Reviewed
"Masahiko Sakai, Keiichirou Kusakari"
"Proc. of the First International Workshop on Higher-Order Rewriting (HOR'02), Copenhagen, Denmark" page： 25 2002.7
Generation of a TRS Implementing the Inverse of Pure Treeless Function Reviewed
"Naoki Nishida, Masahiko Sakai, Toshiki Sakabe"
Computer Software Vol. 19 ( 1 ) page： 29-33 2002.1
Decidability of root-needed strategy in priority term rewriting systems
"Tsuyoshi Suzuki, Masahiko Sakai, Toshiki Sakabe"
Technical Report of IEICE Vol. COMP2001-80 page： 49-55 2002.1
Proving Behavioral Equivalence for Weakly Complete Behavioral Specifications by Implicit Induction
"Yasushi Kano, Masahiko Sakai, Toshiki Sakabe"
Technical Report of IEICE Vol. COMP2001-79 page： 41-47 2002.1
Descendants and Head Normalization of Higher-Order Rewrite Systems
"Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa"
Technical Report of IEICE Vol. COMP2001-82 page： 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 Vol. COMP2001-67 page： 33-40 2001.12
Generation of Inverse Term Rewriting Systems for Pure Treeless Functions Reviewed
"Naoki Nishida, Masahiko Sakai, Toshiki Sakabe"
"Proc. of the International workshop on Rewriting in Proof and Computaion, Sendai, Japan" page： 188-198 2001.10
On New Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems Reviewed
"Masahiko Sakai, Keiichirou Kusakari"
"Proc. of the International Workshop on Rewriting in Proof and Computation (RPC'01), Sendai, Japan" page： 176-187 2001.10
An Extension of Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems Reviewed
"Masahiko Sakai, Yoshitsugu Watanabe, Toshiki Sakabe"
IEICE Trans. on Information and Systems Vol. E84-D ( 8 ) page： 1025-1032 2001.8
Generation of a Conditional TRS Implementing the Inverses of Pure Treeless Functions
"Naoki Nishida, Masahiko Sakai, Toshiki Sakabe"
Technical Report of IEICE Vol. COMP2001-14 page： 9-16 2001.6
Confluence of Orthogonal Metaterm Rewriting Calculus with Rules Containing rules Reviewed
"Sun Hui Hong, Masahiko Sakai, Toshiki Sakabe"
Computer Software Vol. 17 ( 6 ) page： 47-51 2000.11
Designing Unlimited Size Resource C-Libraries Freeing Users from GC Annoyance
"Naoki Nishida, Masahiko Sakai, Toshiki Sakabe"
Technical Report of IEICE Vol. SS2000-9 page： 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
直交メタ項書換え計算のデベロップメントと合流性
洪順姫、酒井正彦、坂部俊樹
電子情報通信学会技術報告 Vol. COMP99-9 page： 65-70 1999.4
順序ソートの自動推論とラベル付けに基づく合流性判定への応用
宮下大、酒井正彦、坂部俊樹
計算モデルとアルゴリズム、数理解析研究所講究録 Vol. 1093 page： 136-141 1999.2
On Completion of Term Set Rewriting Systems
"Hideto Kasuya, Masahiko Sakai, Shinichirou Yamamoto, Kiyoshi Agusa"
Technical Report of IEICE Vol. SS98-66 page： 25-31 1998.12
Semantics and Strong Sequentiality of Priority Term Rewriting Systems Reviewed
"Masahiko Sakai, Yoshihito Toyama"
Theoretical Computer Science Vol. 208 page： 87-110 1998.11
An Improved Recursive Decomposition Ordering for Higher-Order Rewrite Systems Reviewed
"Munehiro Iwami, Masahiko Sakai, Yoshihito Toyama"
IEICE Trans. on Information and Systems Vol. E81-D ( 9 ) page： 988-996 1998.9
Index Reduction of Overlapping Strongly Sequential Systems Reviewed
"Takashi Nagaya, Masahiko Sakai, Yoshihito Toyama"
IEICE Trans. on Information and Systems Vol. E81-D ( 5 ) page： 419-426 1998.5
Modularity of Termination in Extended Hierarchical Combination of Term Rewriting Systems
"Kenji Ohno, Nobuo Kawaguchi, Masahiko Sakai, Toshiki Sakabe, Yasuyoshi Inagaki"
Technical Report of IEICE Vol. SS97-84 page： 57-61 1998.3
Proing Termination of Higher Order Rewriting Systems based on Dependency Pairs
"Yoshitsugu Watanabe, Nobuo Kawaguchi, Masahiko Sakai, Toshiki Sakabe, Yasuyoshi Inagaki"
Technical Report of IEICE Vol. SS97-85 page： 63-70 1998.3
On Confluent Property of Type-IIn Conditional Term Rewrite Systems
"Tohru Nishimura, Masahiko Sakai, Toshiki Sakabe"
Technical Report of IEICE Vol. COMP97-84 page： 45-49 1998.1
Left-Incompatible Term Rewriting Systems and Functional Strategy Reviewed
Masahiko Sakai
IEICE Trans. on Information and Systems Vol. E80-D ( 12 ) page： 1176-1182 1997.12
Term Set Rewriting Systems and their Confluent Property Reviewed
"Hideto Kasuya, Masahiko Sakai, Shinichirou Yamamoto, Kiyoshi Agusa"
Transaction of IEICE Vol. J80-D-I ( 4 ) page： 325-334 1997.4
An Improved Recursive Decomposition Ordering for Higher-Order Rewrite Systems
"Munehiro Iwami, Masahiko Sakai, Yoshihito Toyama"
"Tech. Rep., IEICE" Vol. COMP96-73 page： 17-24 1997.1
On the Confluence Property of Conditional Term Rewriting Systems Reviewed
"Yoshitaka Takahashi, Masahiko Sakai, Yoshihito Toyama"
Transaction of IEICE Vol. J79-D-I ( 11 ) page： 897-902 1996.11
Semantics and Strong Sequentiality of Priority Term Rewriting Systems Reviewed
"Masahiko Sakai, Yoshihito Toyama"
"Proc. on Rewriting Techniques and Applications at New Brunswick NJ USA, LNCS" Vol. 1103 page： 377-391 1996.7
Index reduction of Overlapping Strong Sequential Systems
"Takashi Nagaya, Masahiko Sakai, Yoshihito Toyama"
"Tech. Rep., IEICE" Vol. COMP96-32 page： 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 page： 160-165 1996.7
Index reduction of Overlapping Strong Sequential Systems
"Takashi Nagaya, Masahiko Sakai, Yoshihito Toyama"
LA Symposium page： 154-165 1996.7
高階項書換え系の停止性について
岩見宗弘，酒井正彦，外山芳人
シンポジウム，情報基礎理論ワークショップ page： 55-60 1996.7
Termination for Associative-Commutative Term Rewriting Systems
"Kenji Nakano, Masahiko Sakai, Yoshihito Toyama"
"Tech. Report, IEICE" Vol. COMP95-104 page： 69-78 1996.3
NVNF-sequeentiality of Left-linear Term Rewriting Systems
"Takashi Nagaya, Masahiko Sakai, Yoshihito Toyama"
"Kyokyuroku, Kyoto University" Vol. 950 page： 153-159 1996.2
高階項書換え系の停止性について
岩見宗弘，酒井正彦，外山芳人
電子情報通信学会技術報告 Vol. COMP95-85 page： 113-121 1996.1
非線形項書換え系の合流性について
草刈圭一朗，酒井正彦，外山芳人
電子情報通信学会技術報告 Vol. COMP95-86 page： 123-129 1996.1
The Semantics of Priority Term Rewriting Systems and their Strong Sequentiality
"Masahiko Sakai, Yoshihito Toyama"
"Technical report, IEICE" Vol. SS95-40 page： 31-38 1996.1
The Functional Strategy: the Extended Left-incompatible Systems
Masahiko Sakai
"Technical Report, IEICE" Vol. SS95-17 page： 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" Vol. 918 page： 109-117 1995.7
An Implementation of TRS on Shared Memory Multipeocessors Reviewed
"Shinichirou Yamamoto, Akira Ishikawa, Masahiko Sakai, Kiyoshi Agusa"
Transaction of IEICE Vol. J78-D-I ( 6 ) page： 559-562 1995.6
A Model for Reuse based on Formal Specifications Reviewed
"Makoto Kawakita, Masahiko Sakai, Shinichirou Yamamoto, Kiyoshi Agusa"
IPSJ Trans. Vol. 36 ( 5 ) page： 1050-1058 1995.5
Error Description on Algebraic Specification and its Automatic Addition Reviewed
"Takeshi Hamaguchi, Masahiko Sakai, Shinichirou Yamamoto, Kiyoshi Agusa"
Transaction of IEICE Vol. J78-D-I ( 3 ) page： 323-330 1995.3
On the modularity of confluent term rewriteing systems with shared construtors
"Akira Kitahara, Masahiko Sakai, Yoshihito Toyama"
Tech. Rep. of IPSJ Vol. 20 ( 2 ) page： 11-20 1995.1
仕様に基づく部品再利用法とその適用
川北誠，酒井正彦，山本晋一郎，阿草清滋
第1回ソフトウェア工学の基礎 ワークショップ Vol. FOSE94 1994.12
On the Confluence of Conditional Term Rewriting Systems
"Yoshitaka Takahashi, Masahiko Sakai, Yoshihito.Toyama"
Tech. Rep. of IEICE Vol. COMP94-65 page： 105-111 1994.11
Decidability of Indices on NVNF-sequential Term Rewriting Systems
"Takashi Nagaya, Masahiko Sakai, Yoshihito Toyama"
Tech. Rep. of IEICE Vol. COMP94-63 page： 87-94 1994.11
On Counfluence of Term Set Rewriting System
"Hideto Kasuya, Masahiko Sakai, Shin'ichiro Yamamoto, Kiyoshi Agusa"
Tech. Rep. of IEICE Vol. SS94-14 page： 17-24 1994.7
On Term Set Rewriting System
"Masahiko Sakai, Hideto Kasuya, Shinichiro Yamamoto and Kiyoshi Agusa"
LA Symposium page： 45-48 1994.7
Similarity on Algebraic Specifications toward Specification Databases
Masahiko Sakai
"Technical Report, JAIST" Vol. IS-RR-94-0012S page： 1-20 1994.5
項の集合の書換え系とKnuth-Bendixの完備化に関する考察
粕谷英人，酒井正彦，山本晋一郎，阿草清滋
電子情報通信学会，ソフトウェアサイエンス研究会 Vol. SS93-41 page： 17-22 1994.1
ソフトウェア操作言語の提案
吉田敦，山本晋一郎，酒井正彦，阿草清滋
電子情報通信学会，ソフトウェアサイエンス研究会 Vol. SS92-18 page： 1-8 1993.1
代数的仕様へのエラー記述の自動付加について
濱口毅，酒井正彦，山本晋一郎，阿草清滋
電子情報通信学会，ソフトウェアサイエンス研究会 Vol. SS92-26 page： 25-32 1993.1
Cover Set Induction for Verifying Algebraic Specifications Reviewed
"Masahiko Sakai, Toshiki Sakabe, Yasuyoshi Inagaki"
Transaction of IEICE Vol. J75-D-I ( 3 ) page： 170-179 1992.3
Similarity on Algebraic Specifications toward Specification Databases
"Masahiko Sakai, Soichi Matsui, Shinichiro Yamamoto, Kiyoshi Agusa"
LA Symposium page： 30-35 1992.2
代数的仕様の検証のための被覆集合帰納法
酒井正彦，坂部俊樹，稲垣康善
情報基礎理論ワークショップ，LAシンポジュウム page： 12-17 1991.2
Algebraic Specification and Automatic Generation of Compilers Reviewed
"Masahiko Sakai, Toshiki Sakabe, Yasuyoshi Inagaki"
Transaction of IEICE Vol. J73-D-I ( 12 ) page： 979-989 1990.12
LASS : Language Processor Generator based on Algebraic Specification Reviewed
"Masahiko Sakai, Toshiki Sakabe, Yasuyoshi Inagaki"
Transaction of IEICE Vol. J73-D-1 ( 10 ) page： 829-838 1990.10
代数的仕様の検証のための被覆集合帰納法
酒井正彦，坂部俊樹，稲垣康善
電子情報通信学会，コンピュテーション研究会 Vol. COMP90-5 1990.5
コンパイル機能を持つTRSインタプリタの実現
酒井正彦，坂部俊樹，稲垣康善
電子情報通信学会，コンピュテーション研究会 Vol. COMP88-93 1989.2
TRSインタプリタの並列最外戦略実現法
山本晋一郎，酒井正彦，坂部俊樹，稲垣康善
電子情報通信学会，コンピュテーション研究会 Vol. COMP88-94 1989.2
代数的仕様における帰納的性質の証明法
酒井正彦，坂部俊樹，稲垣康善
電子情報通信学会，コンピュテーション研究会 Vol. COMP88-86 page： 83-92 1989.1
Direct Implementation System of Algebraic Specification of Abstract Data Types Reviewed
"Masahiko Sakai, Toshiki Sakabe, Yasuyoshi Inagaki"
Computer Software Vol. 4 ( 4 ) page： 16-27 1987.10
An Algebraic Approach to Specification of Programming Languages and Automatic Generation of Language Processors Reviewed
"Yasuyoshi Inagaki, Hidehiko Kita, Masahiko Sakai, Toshiki Sakabe"
Proceedings of Regional Symposium on Computer Science and its Applications in Thai page： 35-1-35-25 1987.1
抽象データ型の代数的仕様の直接実現系Cdimple
酒井正彦，坂部俊樹，稲垣康善
電子通信学会技術研究報告，コンピュテーション研究会 Vol. COMP96-67 page： 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" Vol. 8601 1986.11
抽象データ型直接実現システムCdimple
酒井正彦，坂部俊樹，稲垣康善
ソフトウエア科学会，関数的プログラミング研究会 Vol. FP-86-07 page： 122-127 1986.11
コンパイラの代数的仕様記述とその自動生成
酒井正彦，坂部俊樹，稲垣康善
情報処理学会研究報告，プログラミング言語研究会 Vol. 86-PL-8-1 page： 1-9 1986.10
コンパイラの代数的仕様記述法
酒井正彦，坂部俊樹，稲垣康善
電子通信学会技術研究報告，ソフトウエアサイエンス研究会 Vol. SS86-9 page： 1-6 1986.7
代数的手法に基づくプログラミング言語の仕様記述法と処理系の自動生成
稲垣康善，北英彦，酒井正彦，坂部俊樹
情報処理学会，知識情報処理シンポジウム論文集 page： 165-174 1985.9
プログラミング言語の代数的仕様記述からのコンパイラ自動生成に関する基礎的考察
酒井正彦，北英彦，坂部俊樹，稲垣康善
言語理論とオートマトン理論シンポジウム論文集 page： 98-101 1985.7
プログラミング言語の代数的仕様記述からのコンパイラ自動生成
酒井正彦，北英彦，坂部俊樹，稲垣康善
電子通信学会技術研究報告，オートマトンと言語研究会 Vol. AL85-10 page： 1-10 1985.5
プログラムの設計
坂部俊樹編、分担執筆酒井正彦（ Role： Joint author）
オーム社 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 Reviewed
Yutaro Nagae, Masahiko Sakai
Informal Proceedings of the 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017) page： 10 2017.9
Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers Reviewed
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) page： 10 2017.9
小栗 滉介, 酒井正彦, 橋本健二
組合せゲーム・パズル(CGP) プロジェクト, 第18回 研究集会 2024.3
Ground Canonical Rewrite Systems Revisited International coauthorship International conference
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 International conference
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 International coauthorship International conference
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 Invited International conference
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 Invited International conference
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 International conference
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 International conference
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) International conference
SAKAI Masahiko
the 35th TRS meeting
CNFs with Elementary Symmetric Clauses and Their SAT Solving International conference
Masahiko Sakai, Yohei Umano and Yoshizane Hino
8th Asian Workshop on Foundation of Software (AWFS 2011)
Introduction to Esoteric Language Malbolge International conference
Japan-Vietnam Workshop on Software Engineering 2010 (JVSE 2010)
例外処理を持つ関数型プログラムの停止性証明法
馬場正貴、酒井正彦、濱口毅、西田直樹、坂部俊樹、草刈圭一朗
第12回プログラミングおよびプログラミング言語ワークショップPPL2010
SATソルバを利用したお絵かきロジックの問題作成支援ツール
長坂哲、伊藤寛之、酒井正彦、草刈圭一朗、西田直樹、坂部俊樹
組合せゲーム・パズルミニプロジェクト 第5回ミニ研究集会、東京
制約付き等式の定理自動証明器の試作
西田直樹，中林直生、酒井正彦、草刈圭一朗，坂部俊樹
日本ソフトウェア科学会 大会
Almost-Non-Overlapping Non-Collapsing Shallow Term Rewriting Systems are Confluent International conference
Masahiko Sakai
Decidability of Termination for CS-TRSs with Right-Linear Right-Shallow DPs International conference
The 33rd Workshop on Term Rewriting Systems, Tsu
Decidability of termination for TRSs with right-shallow DPs International conference
The 31st Workshop on Term Rewriting Systems, Yamanaka
On confluent property of shallow term rewriting systems International conference
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 International conference
The 2nd Austria - Japan Summer Workshop on Term Rewriting, Obergurgl
Straight line programming in Malbolge International conference
The 28th Workshop on Term Rewriting Systems, Katayamazu
On decidability of termination International conference
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 International conference
The 24nd Workshop on Term Rewriting Systems, Matsue
右辺のみに現れる変数を持つ右線形オーバーレイ項書換え系の最左最内ナローイングによる正規形の計算
西田直樹、酒井正彦、坂部俊樹
2003年度夏のLAシンポジウム
Decidability of termination for TRSs with right-shallow DPs International conference
The 31st Workshop on Term Rewriting Systems, Yamanaka
n箇所パターン照合関数のDeforestationに基づく効率化
中村敏広、酒井正彦、坂部俊樹
シンポジウム，情報基礎理論ワークショップ
Confluence of Weakly Orthogonal CTRSs with Extra Variables
LA symposium
Constrained Rewriting and SMT: Emerging Trends in Rewriting
2012.5 - 2014.3
Grant type：Competitive
Austria - Japan Summer Workshop on Term Rewriting
2010.8
Grant type：Competitive
項書換え理論の関数型言語への応用
2002.4
日東学術振興財団第19回助成金
Grant type：Competitive
関数型言語における計算戦略
2000.4 - 2002.3
栢森情報科学振興財団研究助成金
Grant type：Competitive
定理自動証明のためのAC停止性
1998 - 1999
財団法人人工知能研究振興財団
Grant type：Competitive
形式言語理論に基づく自動採譜 International coauthorship
Grant number：20H04302 2020.4 - 2025.3
科学研究費補助金 基盤研究(B)
Authorship：Principal investigator Grant type：Competitive
Grant amount：\15990000 （ Direct Cost: \12300000 、 Indirect Cost：\3690000 ）
データベース上の制約プログラミングのためのSQL言語の拡張とその処理系
Grant number：17H01721 2017.4 - 2020.3
科学研究費補助金 基盤研究(B)
Authorship：Principal investigator
Grant amount：\11050000 （ Direct Cost: \8500000 、 Indirect Cost：\2550000 ）
耐改竄性をもつプログラム言語とそのプログラム開発手法の研究
2014 - 2017.3
科学研究費補助金 挑戦的萌芽研究
酒井 正彦
Authorship：Principal investigator
ソフトウェアプロテクションのための超難読言語Ｍａｌｂｏｌｇｅの研究
2010 - 2013.3
科学研究費補助金 挑戦的萌芽研究，課題番号：22650003
酒井 正彦
Authorship：Principal investigator
関数型言語の解析・検証・効率的実行のための書換え系理論の研究
2006.4 - 2010.3
科学研究費補助金 基盤研究（Ｃ），課題番号：18500011
酒井 正彦
Authorship：Principal investigator
関数型言語の解析・検証・効率的実行のための書換え系理論の研究
2003.4 - 2006.3
科学研究費補助金 基盤研究（Ｃ），課題番号：15500007
酒井 正彦
Authorship：Principal investigator
関数型言語における計算戦略
1999.4 - 2003.3
科学研究費補助金 基盤研究(C)(2)・11680352
代数的手法に基づくソフトウェアの検証の基礎的研究
1995 - 1998
科学研究費補助金 一般研究(C)(2)・07680350
プログラム理論特論
2001
情報基礎論第1及び演習
1999
プログラム理論特論
1999
情報基礎論第1及び演習
1998
情報基礎論第1及び演習
1997
計算機科学特論Ｉ
2004.4 - 2005.3 （Kochi University）
計算機科学特論Ｉ
2003.4 - 2004.3 （Kochi University）
計算機科学特論Ｉ
2002.4 - 2003.3 （Kochi University）
計算機科学特論Ｉ
2001.4 - 2002.3 （Kochi University）
計算機科学特論Ｉ
2000.4 - 2001.3 （Kochi University）
プログラミングII
2000.4 - 2001.3 （Aichi Prefectural University）
プログラミングI
2000.4 - 2001.3 （Aichi Prefectural University）
プログラミングI
1999.4 - 2000.3 （Aichi Prefectural University）
プログラミングII
1999.4 - 2000.3 （Aichi Prefectural University）
プログラミングI
1998.4 - 1999.3 （Aichi Prefectural University）
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）
