[logic-ml] TPP10 (Theorem Proving and Provers Meeting) Program

[Jacques Garrigue]

名古屋大学で開催されるTPP10の案内をお送りします。

TPP10 幹事
Jacques Garrigue

=========================================================================
Call for participation for TPP 2010 in Nagoya

第6回 TPPミーティングを 11月 25日(木)-26日(金) に名古屋大学にて開催します．
このミーティングは，2005年から年に1回開催され，
定理証明系を作っている人から使う側の人まで幅広い人たちが集まり，
様々な側面からの話をしてアイディアの交換をしてきたものです．

日時：11月25日(木) 13:00頃 〜 11月26日(金) 15:00頃　
場所：名古屋大学 多元数理科学研究科 理学部A館 A428号室
URL: http://www.math.nagoya-u.ac.jp/~garrigue/tpp10/

プログラムを同封しましたので、参加されたい方はご連絡を下さい．

申込み・問い合わせ先：tpp10 at math.nagoya-u.ac.jp (Jacques Garrigue)
=========================================================================

The 6th Theorem Proving and Provers meeting will be held on November
25(Thu) - 26(Fri), 2010 at Nagoya University.

Time:  11/25 around 1pm to 11/26 around 3pm
Place: Nagoya Univ. Grad. School of Mathematics, Bld. Sci. A, Room A428
URL: http://www.math.nagoya-u.ac.jp/~garrigue/tpp10/

The program is enclosed. If you would like to attend, please drop me a
mail.

Submission/questions to: tpp10 at math.nagoya-u.ac.jp (Jacques Garrigue)
=========================================================================

TPP'10 Program

Thursday, November 25

13:00-14:20
Balance Condition on Weight-Balanced Trees
 Youichi Hirai (University of Tokyo), Kazuhiko Yamamoto (IIJ Innovation
 Institute)
Maximal Completion
 Dominik Klein (JAIST)

14:40-16:00
Formal Scientific Reasoning
 Rene Vestergard (JAIST)

16:20-17:40
Representing Polymorphic Higher-Order Abstract Syntax in Agda and Presheaves
 Makoto Hamana (Gunma University)
Simpoulet: an attempt at proving behavioural bisimulations in Coq
 Jacques Garrigue (Nagoya University) and Pierre-Marie Pedrot (ENS Lyon)

18:30-20:30
 Party

Friday, November 26

9:00-10:20
IsaFoR/CeTA - Automatic Certification of Termination Proofs
 Christian Sternagel (University of Innsbruck)
Complexity Analysis by Rewriting for Exponential Time
 Naohi Eguchi (JAIST)

10:40-12:00
証明支援器Coqのシステム開発実務への適用 (Applying Coq to practial
software development)
 Yoshihiro Imai (IT Planning)
Instrumenting Error-correcting codes with SSReflect (work in progress)
 Reynald Affeldt (AIST)

13:20-14:00
Formalizing Regular Expression Matching in Isabelle/HOL
 Yasuhiko Minamide (Tsukuba University)

14:00-15:00
 Solutions to TPPmark10
 (The problem can be found at the above URL)