Program of 51st TRS meeting in Sōunkyō

Program

14:30 – 15:00	Registration
15:00 – 15:05	Opening
15:05 – 17:00	Session 1 (chair: T. Aoto)
15:05	On Inversion and Determinization via Context-Free Expressions Naoki Nishida Nagoya U.
15:55	On Formalizing Logically Constrained TRSs in Isabelle/HOL Ryota Nakayama Nagoya U.
16:30	Simplification of ROBDD Generated by Binary Base Form Pseudo-Boolean Constraints Jiaqi He Nagoya U.

9:00 – 10:35	Session 2 (chair: N. Nishida)
9:00	An Extension of the Parallel Closedness Theorem Kiraku Shintani JAIST
9:50	Termination in FORT: Infinity Predicate Formalization Aart Middeldorp U. Innsbruck
10:35 – 10:50	Break
10:50 – 12:00	Session 3 (chair: K. Nakazawa)
10:50	Comparison of Uniform Semi-Unification and Rational Unification Revisited Munehiro Iwami Shimane U.
11:25	Rhythm quantization as an efficiently-solvable optimization problem Masahiko Sakai Nagoya U.
12:00 – 14:00	Lunch Break
14:00 – 15:15	Free Discussion
15:15 – 15:30	Break
15:30 – 17:00	Free Discussion

9:00 – 10:35	Session 4 (chair: A. Middeldorp)
9:00	On Proving Termination of Bit-Vector LCTRSs Donghoon Shin Nagoya U.
9:35	Productivity in Finitary Rewriting Akihisa Yamada NII
10:20 – 10:35	Break
10:35 – 12:00	Session 5 (chair: M. Iwami)
10:35	Development Closedness and Proofclusters Nao Hirokawa JAIST
11:10	Level-Confluence of Left-Linear Overlapping CTRSs Takahito Aoto Niigata U.
12:00 – 14:00	Lunch Break
14:00 – 15:05	Session 6 (chair: A. Yamada)
14:00	Commutative Rewrite Steps in Rational Term Rewriting Mamoru Ishizuka Niigata U.
14:35	On Cut-Elimination in Cyclic-Proof System Koji Nakazawa Nagoya U.
15:05 – 15:20	Break
15:20 – 16:50	Session 7 (chair: N. Hirokawa)
15:20	Confluence Proof of λμ Calculus by Z Theorem Yuuki Honda Nagoya U.
15:55	A Simple Proof for Kahrs-Smith's Theorem Michio Oyamaguchi Nagoya U.
16:30 – 16:50	Business Meeting
16:50 – 17:00	Closing