Program
February 27
14:00 – 14:30 | Registration |
14:30 – 16:00 | Session 1 (chair: Akihisa Yamada) |
Complexity Results on Register Context-Free Grammars and Register Tree Automata Ryoma Senda Nagoya U. | |
Deciding Unique Normal Forms for Shallow Rewrite Systems Fabian Mitterwallner U. Innsbruck | |
16:00 – 16:15 | Coffee Break |
16:15 – 18:00 | Session 2 (chair: Mizuhito Ogawa) |
Confluence for Right-Ground Composable TRSs Kiraku Shintani JAIST | |
17:00 – 18:00 |
50 TRS Meetings in Japan Aart MiddeldorpU. Innsbruck |
February 28
9:00 – 10:30 | Session 3 (chair: Aart Middeldorp) |
Well-Quasi-Ordering and REgularity Mizuhito Ogawa JAIST | |
On an abstract framework for proving confluence of nonterminating systems Masahiko Sakai Nagoya U. | |
10:30 – 10:45 | Coffee Break |
10:45 – 12:15 | Session 4 (chair: Takahito Aoto) |
Comparison of Uniform Semi-Unification and Rational Unification Munehiro Iwami Shimane U. | |
Transformations for Word Problems Yusuke Oi JAIST | |
12:15 – 14:00 | Lunch Break |
14:00 – 15:30 | Session 5 (chair: Nao Hirokawa) |
MaedMax: A Maximal Ordered Completion Tool Sarah Winkler U. Innsbruck | |
Proving Infeasibility by Basic Narrowing Naoki Nishida Nagoya U. | |
15:30 – 15:45 | Coffee Break |
15:45 – 17:15 | Session 6 (chair: Naoki Nishida) |
Fixed point characterization of soundness and completeness for martingale approximation techniques Toru Takisaka NII | |
Weighted Rewriting Akihisa Yamada NII | |
17:15 – 17:30 | Coffee Break |
17:30 – 18:15 | Session 7 (chair: David Sprunger) |
Machine Learning for Rewriting Cezary Kaliszyk U. Innsbruck |
March 1
9:00 – 10:00 | Session 8 (chair: Munehiro Iwami) |
A Proof Assistant for Constrained Rewriting Induction with Lemma Generation Based on Equality Derivation Donghoon Shin Nagoya U. | |
Rewriting dataflow diagrams David Sprunger NII | |
10:00 – 10:15 | Coffee Break |
10:15 – 11:45 | Session 9 (chair: Masahiko Sakai) |
Certified ACKBO Alexander Lochmann U. Innsbruck | |
Weighted Path Relation for S-Expression Rewriting System Kohei Nishino Niigata U. | |
11:45 – 13:30 | Lunch Break |
13:30 – 15:00 | Session 10 (chair: Sarah Winkler) |
TBA Ryota Nakayama Nagoya U. | |
Composing Proof Terms: Equivalence and Automation Aart Middeldorp U. Innsbruck | |
15:00 – 15:15 | Coffee Break |
15:15 – 16:45 | Session 11 (chair: Cezary Kaliszyk) |
TBA Takahito Aoto Niigata U. | |
Left-Normal Translation Nao Hirokawa JAIST | |
16:45 – 17:00 | Coffee Break |
17:00 – 17:45 | Session 12 (chair: Kiraku Shintani) |
Is a Simple Proof Possible for Kahrs-Smith's Theorem? Michio Oyamaguchi Nagoya U. |
March 2
9:30 – 12:00 | Free Discussion (chair: Akihisa Yamada) |