caml-list - the Caml user's mailing list
 help / Atom feed
* [Caml-list] [Call for Participation] The Coq Workshop 2019
@ 2019-08-01  0:55 Jacques Garrigue
  0 siblings, 0 replies; 1+ messages in thread
From: Jacques Garrigue @ 2019-08-01  0:55 UTC (permalink / raw)
  To: Mailing List OCaml; +Cc: Reynald AFFELDT

The Coq Workshop 2019: Call for Participation
Colocated with the 10th International Conference on
Interactive Theorem Proving (ITP 2019), Portland, OR, USA

We are pleased to invite you to participate in the Coq workshop 2019,
which will be held on September 8 2019, in Portland, OR, USA.
The Coq workshop is part of ITP 2019 (

- The Coq workshop 2019 is the 10th Coq Workshop.  The Coq Workshop
 series ( brings together Coq
 ( users, developers, and contributors.  While
 conferences usually provide a venue for traditional research papers,
 the Coq Workshop focuses on strengthening the Coq community and
 providing a forum for discussing practical issues, including the
 future of the Coq software and its associated ecosystem of libraries
 and tools. Thus, the workshop will be organized around informal
 presentations and discussions, supplemented with invited talks.

- Invited talk:
 + Nicolas Tabareau: Not a single proof assistant for all, but proof assistants for everyone
- Discussion session with the Coq development team
- Accepted talks:
 + Kazuhiko Sakaguchi. Validating Mathematical Structures
 + Akira Tanaka. A Gallina Subset for C Extraction of Non-structural Recursion
 + Christian Doczkal and Damien Pous. Graph Theory in Coq: Minors, Treewidth, and Isomorphisms
 + Bruno Bernardo, Raphaël Cauderlier, Basile Pesin, Zhenlei Hu and Julien Tesson.
   Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts
 + Reynald Affeldt, Jacques Garrigue, Xuanrui Qi and Kazunari Tanaka.
   Experience Report: Type-Driven Development of Certified Tree Algorithms in Coq
 + Enrico Tassi and Erik Martin-Dorel. SSReflect in Coq 8.10
 + Matthieu Sozeau, Yannick Forster, Simon Boulier, Nicolas Tabareau and Théo Winterhalter.
   Coq Coq Codet!
 + Florian Steinberg and Holger Thies.
   Computable analysis, exact real arithmetic and analytic functions in Coq
 + Florian Steinberg. _Some formal proofs about summable sequences in Coq
- See for the schedule.

- Early registration is before [2019-08-04 Sun]
- See the ITP 2019 website for registration information:

Program Committee:
- Reynald Affeldt (AIST)
- Christian Doczkal (CNRS - LIP, ENS Lyon)
- Jacques Garrigue (Nagoya University)
- Chantal Keller (LRI, Univ. Paris-Sud)
- Dominique Larchey-Wendling (CNRS, Loria)
- Gregory Malecha (BedRock Systems Inc.)
- Pierre-Marie Pédrot (INRIA)
- Ilya Sergey (Yale-NUS College and NUS School of Computing)
- John Wiegley (DFINITY)

Organization contact (co-chairs):
reynald.affeldt AT, garrigue AT

^ permalink raw reply	[flat|nested] 1+ messages in thread

only message in thread, back to index

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-08-01  0:55 [Caml-list] [Call for Participation] The Coq Workshop 2019 Jacques Garrigue

caml-list - the Caml user's mailing list

Archives are clonable: git clone --mirror

AGPL code for this site: git clone public-inbox