(Last update: February 26, 2018)
Program
| Meeting room: | かとれあ (Katorea), located on the 2nd floor |
Sunday, February 25
| 13:30 – 14:00 | Registration | |
| 14:00 | Opening | |
| 14:00 – 15:20 | Session 1 (chair: Takahito Aoto) | |
| Confluence by Strong Commutation with Disjoint Parallel Reduction(30min) | ||
| Kentaro Kikuchi(Tohoku University) | ||
| SN+CR Proof of Extensional lambda-calculus with Unit Types by a Relativized Typed Operational Semantics(30 min) | ||
| Yohji Akama (Tohoku University) | ||
| 15:20 – 15:40 | Coffee Break | |
| 15:40 – 17:00 | Session 2 (chair: Sarah Winkler) | |
| On probabilistic term rewriting(30 min) | ||
| Akihisa Yamada(NII) | ||
| Confluence via Rewrite Strategies(30 min) | ||
| Nao Hirokawa(JAIST) | ||
| 18:30 – 20:30 | Dinner |
Monday, February 26
| 7:00 – 8:45 | Breakfast | |
| 8:45 – 10:20 | Session 3 (chair: Yoshihito Toyama) | |
| FORT 2.0(45 min) | ||
| Aart Middeldorp(University of Innsbruck) | ||
| Completion for Logically Constrained Rewriting(30 min) | ||
| Sarah Winkler(University of Innsbruck) | ||
| 10:20 – 10:40 | Coffee Break | |
| 10:40 – 12:00 | Session 4 (chair: Nao Hirokawa) | |
| ComplCoq: Rewrite Hint Construction with Completion in Coq(20 min) | ||
| Keisuke Nakano(University of Electro-Communications) | ||
| Reversibility in Process Calculi | ||
| Shoji Yuen(Nagoya University) | ||
| 11:50 – 13:30 | Lunch Break | |
| 13:30 – 14:50 | Session 5 (chair: Akihisa Yamada) | |
| Formalizing the SR Transformation and Its Reduction-Preservation within Isabelle/HOL(30 min) | ||
| Ryota Nakayama(Nagoya University) | ||
| Formalizing Ground Tree Tranducers in Isabelle(30 min) | ||
| Venkata Hanumanta Prathamesh Turaga(University of Innsbruck) | ||
| 14:50 – 15:10 | Coffee Break | |
| 15:10 – 17:10 | Session 6 (chair: Aart Middeldorp) | |
| Alternating Finite Automata and Antichain Algorithm (30 min) | ||
| Kei Shirakizawa(JAIST) | ||
| Lemma Generation Methods for Inductive Theorem Proving(30 min) | ||
| Hiroto Kato(Niigata University) | ||
| Head Normalization by Random Descent | ||
| Yoshihito Toyama(Tohoku University) | ||
| 18:30 – 20:30 | Dinner |
Tuesday, February 27
| 7:00 – 9:00 | Breakfast | |
| 9:00 – 10:20 | Session 7 (chair: Kentaro Kikuchi) | |
| Syntactic Unification over Rational Terms Revisited(30 min) | ||
| Munehiro Iwami(Shimane University) | ||
| The Church--Rosser theorem and analysis of reduction length(30 min) | ||
| Ken-etsu Fujita(Gunma University) | ||
| 10:20 – 10:40 | Coffee Break | |
| 10:40 – 12:00 | Session 8 (chair: Munehiro Iwami) | |
| Proving Unique Normal Forms w.r.t. Conversion of Term Rewriting Systems Automatically(30 min) | ||
| Takahito Aoto(Niigata University) | ||
| Non-ω-overlapping TRSs are non-E-overlapping(30min) | ||
| Michio Oyamaguchi(Nagoya University) | ||
| 12:00 | Closing |