57th TRS Meeting (and 18th TPP Meeting)

September 27 (Tue) - 29 (Thu), 2022
Eiheiji, Fukui, Japan

News

About TRS Meeting

The Term Rewriting Meeting, traditionally called ``TRS Meeting'', is a biannual informal workshop that aims at promoting the research on rewriting and related areas. Participants are encouraged to present their recent activities, observations, and results at the meeting (in English), however, it is perfectly acceptable to explain a paper written by someone else.

Information

Basic Information

dates:
September 27 (Tue) 14:00 - September 29 (Thu) 12:00, 2022
style:
hybrid meeting (you may choose on-site participation or online participation)
note:
The meeting is co-located with TPP 2022.

About on-site participation

venue:
Zen no Sato - Mirai (禅の里・笑来)
Suwama 4-11, Eiheijichou, Yoshidagun, Fukui, Japan (福井県吉田郡永平寺町諏訪間4−11)
capacity:
≤ 15 participants. First come, first served. So register now!
fee:
student: 8,000 JPY per night
non-student: 10,000 JPY per night

About online participation

meeting system:
video meeting system Webex
meeting URL:
We sent you its URL by email. Please let us know if you do not find the email.
fee
free

Program

September 27 (Tue)

14:00
opening time of the seminar room
14:20 - 15:40
1st session (chair: Nao Hirokawa)
Hedge Transducers (30 min)
Akihisa Yamada
Reformulating the Dependency Pair Method as Reduction Orders (30 min)
Ziyu Guo
16:00 - 17:20
2nd session (chair: Takahito Aoto)
Rewriting of Rational Terms by Tree Transducer (30 min)
Munehiro Iwami (online)
Duplicate Checking for Rewrite Systems (30 min)
Nao Hirokawa
17:40 - 19:00
3rd session (chair: Munehiro Iwami)
Combination of Critical Pair Systems and Outside Closedness (30 min)
Kiraku Shintani
Rewriting Induction Framework for Proving Inductive Theorems (30 min)
Takahito Aoto
19:30 - 21:00
banquet
21:00 - 21:30
free discussion

September 28 (Wed)

14:00 - 15:20
4th session (chair: Nao Hirokawa)
Cut-elimination for a Hypersequent Calculus for First-order Gödel Logic over [0, 1] with Δ (30 min)
Norbert Preining
Interpretation Orders for Applicative Term Rewrite Systems (30 min)
Teppei Tanaka
15:40 - 17:00
5th session (chair: Kazuhisa Nakasho)
Hyper-Normalization via Context-Sensitive Rewriting (30 min)
Teppei Saito
On Transforming Imperative Programs into LCTRSs via Injective Functions from Configurations to Terms (30 min)
Naoki Nishida (online)
17:20 - 19:00
6th session (chair: Naoki Nishida)
AC-Completion for Left-Linear TRSs (30 min)
Johannes Niederhauser (online)
Development Closed Critical Pairs: Formalization and Certification (45 min)
Aart Middeldorp (online)
19:30 - 21:30
banquet & business meeting
FYI:

September 29 (Thu)

See the program of the TPP meeting.

Access

Fukui Station to venue

Echizen Railway operates the line between Fukui (福井) and Eiheiji-guchi (永平寺口) every half hour; 460 yen. The venue is a walking distance from Eiheiji-guchi Station (about 10 minutes).

To Fukui Station by train or bus

From Komatsu Airport to Fukui Station

The following would be fit for flights of ANA754, HND1015 → KMQ1125. A limousine bus (1,400 yen) bound for Fukui Station is available at the airport, but the connection is not suited for attending the first day of the meeting.

Registration (closed)

Please send the following registration form to Nao Hirokawa by email. The deadline is August 30 (Tue), 2022.
----------------------------------------------------------------------
              Registration Form of the 57th TRS Meeting

Name:
Affiliation:

participation: [on-site / online]
If you choose on-site, please leave one: [Male / Female] 

Title of talk (*):
Duration of talk (*):

Requests/comments (on foods, partial participation, etc.):

----------------------------------------------------------------------
The items marked with * can be sent later.

Participants

Takahito Aoto (Niigata University) on-site
Ziyu Guo (JAIST) on-site
Nao Hirokawa (JAIST) on-site
Munehiro Iwami (Shimane University) online
Aart Middeldorp (University of Innsbruck) online
Johannes Niederhauser (University of Innsbruck) online
Naoki Nishida (Nagoya University) online
Mizuhito Ogawa (JAIST) on-site
Norbert Preining (Mercari Inc, Japan) on-site
Teppei Saito (JAIST) on-site
Kiraku Shintani (JAIST) on-site
Teppei Tanaka (JAIST) on-site
Akihisa Yamada (AIST) on-site

Contact

18th TPP Meeting

Announce

Call for TPP online presentations.

About TPP Meeting (Theorem Proving and Provers Meeting)

TPP has started 2005 as an annual meeting on theorem proving and provers, such as Isabelle, Coq, and Mizar. We regard the discussions during the meeting to be most important. As such, not only the talks about completed work, but those about ongoing work and half-baked work are also welcome. We hope all participants would consider giving a talk. TPP 2022 aims formal proofs of mathematical theorems. For instance, Mizar has long tradition on formalizing mathematics, and AFP (Archives of Formal Proofs) of Isabelle continuously increases. Coq as well.

TPP Program

発表は、基本、日本語の見込みです。オンライン参加申し込みは当日まで受け付けます。

September 28 (Wed)

Online session
 9:30 - 10:00 
Lean による結び目理論の形式化の試み
南出靖彦(東工大)
10:00 - 10:30
Interpreting OCaml GADTs into Coq
Jacques Garrigue(名古屋大)
10:40 - 11:40
[Panel discussion] Hybrid session
Formal mathematics on various theorem provers
e.g., Mizar(中正), LEAN(南出), Coq (Garrique), Isabelle/HOL(小川)
[Introduction slides]
[Formal proof archives]
11:40 - 12:00
Report on TPPmark

September 29 (Thu)

Hybrid session
 9:30 -  9:45
Complete axiomatization of series-parallel graphs (survey)
小川瑞史 (JAIST)
 9:45 - 10:30
Information-Theoretic Metrices on Theorem Spaces
中正和久(山口大)
10:40 - 11:10
Isabelle/HOL による確率的プログラム検証
平田路和(東工大)
11:10 - 11:40
Formalizing Actuarial Mathematics in Isabelle/HOL
伊藤洋介(SOMPOひまわり生命保険)
12:00
closing

TPP participants

石黒 吉洋 (名古屋大学) online
伊藤 洋介 (SOMPOひまわり生命保険) online
宇田 津孝介 (JAIST) online
太田 悠 (法政大学) on-site
小川 瑞史 (JAIST) on-site
金沢 誠 (法政 大学) online
Jacques Garrigue (名古屋大学) online
佐藤 雄大 (名古屋大学 卒業生) online
十文字 遼 online
龍田 真 (NII) on-site
田中 哲 (AIST) on-site
辻 陽介 (北見工業大学) online
中正 和久 (山口大学) on-site
中村 薫 (名古屋大学) online
平田 路和 (東京工業大学) on-site
毎田 詠人 (名古屋大学) online
南出 靖彦 (東京工業大学) online
溝口 佳寛 (九州大学) online
三輪 忠義 (放送大学・東京大学) online
山本 光晴 (千葉大学) online
Qi Xuanrui (名古屋大学) online
...

TPP mark

TPP mark is a challenge for the meeting. TPP mark of TPP 2022 is here.

Past TPP

TPP2021 / TPP2020 / TPP2019 / TPP2018 / TPP2017 / TPP2016 / TPP2015 / TPP2014 / TPP2013 / TPP2012 / TPP2011 / TPP2010 / TPP2009 / TPP2008 / TPP2007 / TPP2006 / TPP2005