皆様、
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)を解いて, ワークショップ中に証明を比べようと思います. 証明支援系, 解き方を問わず, みなさまの多くの証明例を募集しています. 証明や質問は下記のメールアドレスに送って下さい. 都合で参加出来ない方の証明の応募も歓迎致します.
申込み・問い合わせ先: [email protected] (溝口佳寛(九州大学))
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: [email protected] (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):
-------------------------------------------------------------------------
=========================================================================