| IEICE Technical Committee Submission System Conference Schedule |
Online Proceedings [Sign in] Tech. Rep. Archives |
All Technical Committee Conferences (Searched in: All Years)
| Committee | Date Time | Place | Paper Title / Authors | Abstract | Paper # | |
| MSS, SS | 2023-01-11 13:30 |
Osaka | (Primary: On-site, Secondary: Online) |
A formal description of a functional language with exception handling, and constrained dependency pairs for the termination proofs Takeshi Hamaguchi, Masahiko Sakai (Nagoya Univ.)  MSS2022-56 SS2022-41 |
This paper proposes a termination-proof method for functional programs with exception handling. First, we give a small s... [more] | MSS2022-56 SS2022-41 pp.66-71 |
| MSS, SS | 2019-01-16 09:50 |
Okinawa | Extending Narrowing Trees to Basic Narrowing in Term Rewriting Yuya Maeda, Naoki Nishida, Masahiko Sakai, Tomoya Kobayashi (Nagoya Univ.) MSS2018-68 SS2018-39 |
Narrowing computation of a term rewriting system is an extension of rewriting by replacing matching with unification, wh... [more] | MSS2018-68 SS2018-39 pp.73-78 |
|
| SS, DC | 2017-10-19 13:15 |
Kochi | Kochi City Culture-plaza CUL-PORT | Towards a lambda-graph rewriting to analyze modification impacts and identify behaviors of dynamically typed procedural languages Koji Yamamoto (Fujitsu Labs.) SS2017-21 DC2017-20 |
Static code analysis, in contrast to dynamic analysis, offers results with higher code coverage to locate differences of... [more] | SS2017-21 DC2017-20 pp.1-6 |
| SS, KBSE, IPSJ-SE [detail] | 2017-07-20 15:50 |
Hokkaido | Polynomial Interpretations to Convert Dependency Chains of Constrained Term Rewriting Systems to Bounded Increasing Sequences of Intergers Tomohiro Sasano, Naoki Nishida, Masahiko Sakai, Tomoya Ueyama (Nagoya Univ.) SS2017-17 KBSE2017-17 |
In dependency pair framework for proving termination of constrained term rewriting systems, polynomial interpretations t... [more] | SS2017-17 KBSE2017-17 pp.139-144 |
|
| SS | 2017-03-10 10:45 |
Okinawa | Proving Confluence of Hierarchical Conditional Term Rewriting Systems without Sufficient Completeness Takayuki Kuroda, Naoki Nishida, Hiroyuki Seki (Nagoya Univ.) SS2016-77 |
A transformational approach to confluence proofs for conditional term rewriting systems (CTRS) has been investigated, bu... [more] | SS2016-77 pp.103-108 |
|
| SS, MSS | 2016-01-26 11:05 |
Ishikawa | Shiinoki-Geihin-Kan | Transforming Constrained Dependency Pairs by Narrowing Tomohiro Sasano, Naoki Nishida, Masahiko Sakai (Nagoya Univ.) MSS2015-57 SS2015-66 |
The dependency pair framework, a method for proving termination of term rewriting systems, has been extended for constra... [more] | MSS2015-57 SS2015-66 pp.123-128 |
| KBSE, SS, IPSJ-SE [detail] | 2015-07-24 11:10 |
Hokkaido | An Equivalent Transformation of Constrained Term Rewriting Systems by Pattern Elimination Takahiro Nagao, Naoki Nishida, Masahiko Sakai (Nagoya Univ.) SS2015-33 KBSE2015-26 |
A constrained term rewriting system, an extension of term rewriting systems, can control application of rules by constra... [more] | SS2015-33 KBSE2015-26 pp.167-172 |
|
| SS | 2015-03-09 09:30 |
Okinawa | OKINAWAKEN SEINENKAIKAN | Sufficient completeness of constructor-based order-sorted parameterized specifications Masaki Nakamura (Toyama Pref. Univ.), Daniel Mircea Gaina, Kazuhiro Ogata, Kokichi Futatsugi (JAIST) SS2014-55 |
CafeOBJ algebraic specification language supports description of specifications whose models are constructor-based order... [more] | SS2014-55 pp.1-6 |
| SS | 2015-03-10 09:30 |
Okinawa | OKINAWAKEN SEINENKAIKAN | A Heuristic to Solve Inverse Unfolding Problem for Functions Dealing with Tree Structure Data Tomofumi Kato, Masanori Nagashima, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe (Nagoya Univ.) SS2014-69 |
Unfold/Fold transformations have been widely used for program transformation, theorem proving, and so on. Unfold and Fo... [more] |
SS2014-69 pp.85-90 |
| SS | 2015-03-10 09:55 |
Okinawa | OKINAWAKEN SEINENKAIKAN | Heuristics for Automatically Proving Commutativity of Function Composition for Constrained Term Rewriting Systems Ryutaro Kuriki, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe (Nagoya Univ.) SS2014-70 |
In proving equations to be inductive theorems of constrained term rewriting systems, we often need appropriate lemmas of... [more] | SS2014-70 pp.91-96 |
| MSS, SS | 2015-01-26 17:45 |
Tottori | Implementing a Conditional Dependency Pair Method for Proving Termination of Functional Programs with Exception Handling Koichi Ota, Takeshi Hamaguchi, Masahiko Sakai (Nagoya Univ.), Akihisa Yamada (AIST), Naoki Nishida, Toshiki Sakabe (Nagoya Univ.) MSS2014-78 SS2014-42 |
In this paper, we discuss implementation of the conditional dependency pair method for proving termination of functional... [more] | MSS2014-78 SS2014-42 pp.55-60 |
|
| SS | 2014-03-11 11:00 |
Okinawa | Tenbusu Naha | Inverse Unfold Problem and Its Heuristic Solving Tomofumi Kato, Masanori Nagashima, Masahiko Sakai, Naoki Nishida (Nagoya Univ.) SS2013-74 |
Unfold/Fold transformations have been widely used for program transformation, theorem proving, and so on.Unfold and Fold... [more] | SS2013-74 pp.13-18 |
| SS | 2014-03-11 13:30 |
Okinawa | Tenbusu Naha | On Detecting Useless Transition Rules of Constrained Tree Automata Yasuhiro Nakano, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Kenji Hashimoto (Nagoya Univ.) SS2013-77 |
Reduction completeness of terms is proved many times in a theorem proving method for constrained term rewriting systems ... [more] | SS2013-77 pp.31-36 |
| SS, KBSE | 2013-07-26 09:30 |
Hokkaido | Conditional Dependency Pair Method for Proving Termination of Functional Programs with Exception Handling Takeshi Hamaguchi, Masahiko Sakai (Nagoya Univ.) SS2013-23 KBSE2013-23 |
We have recently proposed a method for proving termination/non-termination properties of eager-evaluation-based function... [more] | SS2013-23 KBSE2013-23 pp.61-66 |
|
| SS | 2013-01-10 13:30 |
Okinawa | Construction of Constrained Tree Automata Recognizing Ground Instances of Constrained Terms Yasuhiro Nakano, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari (Nagoya Univ.) |
A theorem proving method for constrained term rewriting systems, which is based on rewriting induction, needs a decision... [more] | SS2012-47 pp.7-12 |
|
| SS | 2012-05-11 11:15 |
Ehime | Ehime Univ. | Static Dependecy Pair Method in Rewriting Systems for Functional Programs with Product, Algebraic Data, and ML-Polymorphic Types Keiichirou Kusakari (Nagoya Univ.) SS2012-9 |
For simply-typed term rewriting systems (STRSs) and higher-order rewrite systems (HRSs) {\em \`a la} Nipkow, we propo... [more] |
SS2012-9 pp.49-54 |
| SS, MSS | 2012-01-26 15:30 |
Kochi | Kochi City Culture-Plaza Cul-Port | On Rewriting Induction for Simply-typed Term Rewriting Systems Akira Ozeki, Keiichirou Kusakari, Tsubasa Sakata, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe (Nagoya Univ.) MSS2011-63 SS2011-48 |
Rewriting induction is a principle of proving inductive theorems by means of derivations obtained by applying inference ... [more] | MSS2011-63 SS2011-48 pp.51-56 |
| SS, MSS | 2012-01-26 16:00 |
Kochi | Kochi City Culture-Plaza Cul-Port | On Usable Rules under Argument Filterings in Higher-Order Rewrite Systems Kazuhiro Ooi, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida (Nagoya Univ.) MSS2011-64 SS2011-49 |
The static dependency pair method is known as a powerful method for proving termination of higher-order rewrite systems ... [more] | MSS2011-64 SS2011-49 pp.57-62 |
| SS | 2010-12-14 16:20 |
Gunma | Ikaho-Onsen Hotel Tenbo | On non-termination proof of right-linear and right-shallow term rewriting systems based on forward narrowing Tatsuya Hattori, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, Toshiki Sakabe (Nagoya Univ.) SS2010-44 |
Detecting non-termination of term rewriting systems based on forward narrowing is used in termination tools such as APro... [more] | SS2010-44 pp.31-36 |
| SS | 2010-10-15 11:00 |
Iwate | Iwate Prefectural Univ. | On DPLL Transition Systems Modulo Equational Theories Tatsuya Baba, Toshiki Sakabe, Naoki Nishida, Keiichirou Kusakari, Masahiko Sakai (Nagoya Univ.) SS2010-36 |
SMT solvers are tools for deciding satisfiability of formulas under given theories such as arrays, lists, queues and so ... [more] | SS2010-36 pp.49-54 |
[Return to Top Page]