<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div dir="ltr" class="">Logic-mlの皆様、名古屋大学のGarrigueです。<br class=""><br class="">Coq Workshop 2019の開催案内をお送りします。<br class="">ご参加をお待ちしております。</div><div dir="ltr" class=""><br class="">早期参加申し込み締切：2019-08-04<br class=""><br class=""><div class="">**********************************************************************<br class="">The Coq Workshop 2019: Call for Participation<br class="">Colocated with the 10th International Conference on<br class="">Interactive Theorem Proving (ITP 2019), Portland, OR, USA<br class="">**********************************************************************<br class=""><br class="">We are pleased to invite you to participate in the Coq workshop 2019,<br class="">which will be held on September 8 2019, in Portland, OR, USA.<br class="">The Coq workshop is part of ITP 2019 (<a href="https://itp19.cecs.pdx.edu/" class="">https://itp19.cecs.pdx.edu/</a>).<br class=""><br class="">Topic:<br class="">- The Coq workshop 2019 is the 10th Coq Workshop. The Coq Workshop<br class=""> series (<a href="https://coq.inria.fr/coq-workshop/" class="">https://coq.inria.fr/coq-workshop/</a>) brings together Coq<br class=""> (<a href="https://coq.inria.fr/" class="">https://coq.inria.fr/</a>) users, developers, and contributors. While<br class=""> conferences usually provide a venue for traditional research papers,<br class=""> the Coq Workshop focuses on strengthening the Coq community and<br class=""> providing a forum for discussing practical issues, including the<br class=""> future of the Coq software and its associated ecosystem of libraries<br class=""> and tools. Thus, the workshop will be organized around informal<br class=""> presentations and discussions, supplemented with invited talks.<br class=""><br class="">Program:<br class="">- Invited talk:<br class=""> + Nicolas Tabareau: Not a single proof assistant for all, but proof assistants for everyone<br class="">- Discussion session with the Coq development team<br class="">- Accepted talks:<br class=""> + Kazuhiko Sakaguchi. Validating Mathematical Structures<br class=""> + Akira Tanaka. A Gallina Subset for C Extraction of Non-structural Recursion<br class=""> + Christian Doczkal and Damien Pous. Graph Theory in Coq: Minors, Treewidth, and Isomorphisms<br class=""> + Bruno Bernardo, Raphaël Cauderlier, Basile Pesin, Zhenlei Hu and Julien Tesson.<br class=""> Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts<br class=""> + Reynald Affeldt, Jacques Garrigue, Xuanrui Qi and Kazunari Tanaka.<br class=""> Experience Report: Type-Driven Development of Certified Tree Algorithms in Coq<br class=""> + Enrico Tassi and Erik Martin-Dorel. SSReflect in Coq 8.10<br class=""> + Matthieu Sozeau, Yannick Forster, Simon Boulier, Nicolas Tabareau and Théo Winterhalter.<br class=""> Coq Coq Codet!<br class=""> + Florian Steinberg and Holger Thies.<br class=""> Computable analysis, exact real arithmetic and analytic functions in Coq<br class=""> + Florian Steinberg. _Some formal proofs about summable sequences in Coq<br class="">- See <a href="https://staff.aist.go.jp/reynald.affeldt/coq2019/" class="">https://staff.aist.go.jp/reynald.affeldt/coq2019/</a> for the schedule.<br class=""><br class="">Registration:<br class="">- Early registration is before [2019-08-04 Sun]<br class="">- See the ITP 2019 website for registration information:<br class=""> <a href="https://itp19.cecs.pdx.edu/registration/" class="">https://itp19.cecs.pdx.edu/registration/</a><br class=""><br class="">Program Committee:<br class="">- Reynald Affeldt (AIST)<br class="">- Christian Doczkal (CNRS - LIP, ENS Lyon)<br class="">- Jacques Garrigue (Nagoya University)<br class="">- Chantal Keller (LRI, Univ. Paris-Sud)<br class="">- Dominique Larchey-Wendling (CNRS, Loria)<br class="">- Gregory Malecha (BedRock Systems Inc.)<br class="">- Pierre-Marie Pédrot (INRIA)<br class="">- Ilya Sergey (Yale-NUS College and NUS School of Computing)<br class="">- John Wiegley (DFINITY)<br class=""><br class="">Organization contact (co-chairs):<br class="">reynald.affeldt AT <a href="http://aist.go.jp" class="">aist.go.jp</a>, garrigue AT <a href="http://math.nagoya-u.ac.jp" class="">math.nagoya-u.ac.jp</a><br class=""><br class=""></div><div class=""><br class=""></div></div><div class=""><br class="webkit-block-placeholder"></div>
-- <br class="">
このメールは Google グループのグループ「sonoteno」に登録しているユーザーに送られています。<br class="">
このグループから退会し、グループからのメールの配信を停止するには <a href="mailto:sonoteno+unsubscribe@googlegroups.com" class="">sonoteno+unsubscribe@googlegroups.com</a> にメールを送信してください。<br class="">
このディスカッションをウェブ上で閲覧するには <a href="https://groups.google.com/d/msgid/sonoteno/19b8a2be-d4a4-4f0b-a68a-d64955ae0f46%40googlegroups.com?utm_medium=email&utm_source=footer" class="">https://groups.google.com/d/msgid/sonoteno/19b8a2be-d4a4-4f0b-a68a-d64955ae0f46%40googlegroups.com</a> にアクセスしてください。<br class="">
</body></html>