) no later than September 30.
The venue can be reached by public transports from Sendai station.
In case of partial participation, let us know.
The Term Rewriting Meeting (TRS Meeting), is a biannual informal workshop that aims at promoting the research on rewriting and related areas including (but not limited to):
Participants are requested to present their recent research activities, observations, and results at the meeting; it is also perfectly acceptable to explain a paper written by someone else. (See TRS Meeting homepage for further information.)
| Date: | November 7-9, 2012 |
| Venue: | Iwanumaya, Akiu onsen, Sendai, Miyagi |
| Fee: | 23,925 yen |
| November 7 (Wed) | |
| 13:00 | bus from Sendai station to the venue |
| 13:45 - 14:05 | |
| opening | |
| appearance of special guests | |
| presentation of the special issue | |
| video messages | |
| 14:05 - 15:15 | |
| Decreasing Proofs by Decreasing Local Peaks | |
| Jean-Pierre Jouannaud and Jiaxiang Liu (Tsinghua University) | |
| Determinization of Conditional Term Rewriting Systems | |
| Masahiko Sakai (Nagoya University) | |
| 15:30 - 17:15 | |
| SMT Encoding of Dependency Pair Method for Maximal Completion | |
| Masahito Kurihara and Haruhiko Sato (Hokkaido University) | |
| Essence of de Bruijn Index | |
| Masahiko Sato (Kyoto University) | |
| Confluence of Explicitly Parallel Language with Control | |
| Yukiyoshi Kameyama (Tsukuba University) | |
| November 8 (Thu) | |
| 9:00 - 10:20 | |
| On Type Inference Problem of 2nd-order Lambda-Calculus | |
| Ken'etsu Fujita (Gunma University) | |
| A Systematic Proof of Strong Normalization for Polymorphic Lambda-Mu-Calculus with Sum and Existential Quantifier Types | |
| Hirofumi Yokouchi (Gunma University) | |
| Process Calculi with Priority | |
| Shoji Yuen (Nagoya University) | |
| 10:35 - 11:55 | |
| From Search to Association - How to Bridge the Isolated Silos of Knowledge - | |
| Akihiko Takano (National Institute of Informatics) | |
| Well-Structured Pushdown Systems (Part 1) | |
| Mizuhito Ogawa (JAIST) | |
| Termination Proof by Fixed Point | |
| Yoshihito Toyama (Tohoku University) | |
| 13:30 - 15:10 | |
| On Terms Representing Sequent Calculus Proofs | |
| Kentaro Kikuchi (Tohoku University) | |
| Minimal Bad Sequences in Isabelle/HOL | |
| Christian Sternagel (JAIST) | |
| A Rewriting Characterisation of the Sub-Polytime Hierarchy | |
| Naohi Eguchi (Tohoku University) | |
| 15:25 - 16:30 | |
| Incremental Proofs of Operational Termination | |
| Masaki Nakamura (Toyama Prefectural University) | |
| Knuth-Bendix Orders, Ordinals, Goodstein Sequences | |
| Aart Middeldorp (University of Innsbruck) | |
| 16:45 - 17:45 | |
| Proving Equality of Streams | |
| Munehiro Iwami (Shimane University) | |
| On the Non-E-overlapping Property of Weak Multi-Layer TRSs | |
| Michio Oyamaguchi (Nagoya University) | |
| November 9 (Fri) | |
| 9:00 - 10:15 | |
| On AC-Compatible Knuth-Bendix Orderings | |
| Akihisa Yamada (Nagoya University) | |
| Computing More Specific Versions of Conditional Rewriting Systems | |
| Naoki Nishida (Nagoya University) | |
| Confluence and E-Unification | |
| Nao Hirokawa (JAIST) | |
| 10:30 - 12:00 | |
| Progress Report on the Rho Property of B Combinators (30 min) | |
| Keisuke Nakano (The University of Electro-Communications) | |
| How to Prove the Equivalence of Simply Typed Term Rewriting Systems without Induction | |
| Yuki Chiba (JAIST) | |
| Termination of Rule-Based Calculi for Uniform Semi-Unification | |
| Takahito Aoto (Tohoku University) | |
| 14:00 | bus from Sendai station to the venue |
Please send the registration form below to Takahito Aoto
(aoto) no later than September 30.
The venue can be reached by public transports from Sendai station.
In case of partial participation, let us know.
----------------------------------------------------------------------
Registration Form of 37th TRS meeting
name:
affiliation:
preference on your room: [A single room is prefered/A shared room is acceptable](choose one)
* title of talk:
* approximate duration of talk (in minutes):
----------------------------------------------------------------------
(The items marked with * can be sent later. )