名古屋大学で開催される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)