[logic-ml] TPP2014: 3rd Announcement and call for participation

[Jacques Garrigue]

皆様、

TPP2014の参加募集案内をお送りします。
参加される方、今週中に返事をいただければと思います。

Jacques Garrigue

=========================================================================

TPP2014: 3rd Announcement and call for participation

=========================================================================
研究集会「高信頼な理論と実装のための定理証明および定理証明器」案内
　　　　　　　　　　　　　　　　　　　(English version is below.)

12月3日(水)-5日(金)に九州大学西新プラザにて, 
研究集会「高信頼な理論と実装のための定理証明および定理証明器」
を開催します. 皆様のご参加をお待ちしています.

日時：2014年 12月3日(水)13:00 〜 12月5日(金)15:00 (予定)
場所：九州大学・西新プラザ
     (福岡市早良区西新2-16-23) http://bit.ly/QdaiNishijin
     福岡空港から地下鉄で西新駅まで約20分, その後, 徒歩約10分.
プログラム：
     詳細は未定ですが, 適宜HPを更新予定です.
     みなさまのご講演をお待ちしています.
     Adam Chlipala氏とCyril Cohen 氏をお招きして,
     ご講演頂く予定です.
      Correct-by-Construction Program Synthesis in Coq,
          Adam Chlipala (MIT, USA).
      Mathematical components and algebraic numbers,
          Cyril Cohen (INRIA Sophia-Antipolis, France).
     御講演を頂く予定です.

参加者と講演の数を大体把握しておきたいと思いますので，参加される方は
10月末までに下の参加申し込みを下記メールアドレスまでお送りください．
参加者には，できるだけ講演していただければと思います．

TPPMARK: 形式証明のための問題を掲示し証明を募集しています.
   皆で問題(PDF)を解いて, ワークショップ中に証明を比べようと思います.
   証明支援系, 解き方を問わず, みなさまの多くの証明例を募集しています.
   証明や質問は下記のメールアドレスに送って下さい.
   都合で参加出来ない方の証明の応募も歓迎致します.

申込み・問い合わせ先:
    tpp2014 at imi.kyushu-u.ac.jp (溝口佳寛(九州大学))

URL: http://imi.kyushu-u.ac.jp/lasm/tpp2014/index_ja.html
    (注. 作成途中です.「TPP2014 数学」で検索してみて下さい.)

-------------------------------------------------------------------------
TPP 2014 参加申し込み

お名前：
ご所属：
講演　：する／しない
懇親会：参加する／参加しない

講演する場合
タイトル：
（講演のタイトルが決まっていなければ，TBAでもかまいません．
決まったらご連絡ください．）
講演希望日: (○/×) 12/3  (○/×) 12/4  (○/×) 12/5

その他(ご意見/ご要望ありましたらお願いします):


-------------------------------------------------------------------------

=========================================================================
Workshop:
Theorem proving and provers for reliable theory and implementations (TPP2014)

This is the call for participation for TPP2014,
to be held on Dec. 3(Wed) - 5(Fri), 2014 at Kyushu University.

Date:  2014/12/03 around 1pm to 12/05 around 3pm
Venue: Nishijin Plaza, Kyushu University
      (2-16-23 Nishijin, Sawara-ku, Fukuoka City)
      http://bit.ly/QdaiNishijinPDF
Invited Speakers:
      Correct-by-Construction Program Synthesis in Coq,
          Adam Chlipala (MIT, USA).
      Mathematical components and algebraic numbers,
          Cyril Cohen (INRIA Sophia-Antipolis, France).

If you are planning to attend the meeting, please send the information
slip below to the indicated address by the end of October.

TPPMARK: A problem for a formal proof is attached in our HP.
   We would like you to solve a problem in your favorite
   theorem prover, and compare solutions at the workshop.
   Please send your proof to the email address below.

Submission/questions to: 
　　　tpp2014 at imi.kyushu-u.ac.jp (Yoshihiro Mizoguchi)

URL: http://imi.kyushu-u.ac.jp/lasm/tpp2014/

-------------------------------------------------------------------------
TPP 2014 Registration

Name:
Affiliation:
Will give a talk:      Yes/No
Will attend the party: Yes/No
Title of the talk: (If it is not decided yet, TBA is OK.)

Which date do you prefer to talk ?
 12/3 (OK/NG)  12/4 (OK/NG)  12/5 (OK/NG)

Requests for the organizer (if any):


-------------------------------------------------------------------------


=========================================================================