The Coq Workshop 2019

coq logo

Location: Portland State University, Portland, OR, USA

Date: September 8, 2019

The Coq workshop 2019 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.

We invite all members of the Coq community to propose informal talks, discussion sessions, or any potential uses of the day allocated to the workshop.

The Call for Proposals in text format

Table of Contents

News

[2019-09-10 Tue]
Add slides to the program.
[2019-08-29 Thu]
Add abstracts to the program.
[2019-08-01 Thu]
Tentative program.
[2019-07-05 Fri]
List of accepted talks.
[2019-07-02 Tue]
Title and abstract for the invited talk; notifications sent to authors.
[2019-06-26 Wed]
Registration information available on the website of ITP 2019.
[2019-06-11 Tue]
Abstract submission closed.
[2019-06-05 Wed]
The submission deadline has been extended to 2019-06-10 (Mon).
[2019-05-31 Fri]
EasyChair is experiencing network problems causing files uploads to be slow. The problem should be fixed within one day. Problem solved on [2019-06-01 Sat].
[2019-05-21 Tue]
We are very happy to announce Dr. ✨Nicolas Tabareau✨ as an invited speaker and to confirm a session with the 🐓Coq development team🐓!

Program

9:00–10:30
  • 9:00 Matthieu Sozeau, Yannick Forster, Simon Boulier, Nicolas Tabareau, Théo Winterhalter. Coq Coq Codet!. abstract, slides
  • 9:30 Akira Tanaka. A Gallina Subset for C Extraction of Non-structural Recursion. abstract, slides
  • 10:00 Florian Steinberg, Holger Thies. Computable analysis, exact real arithmetic and analytic functions in Coq. abstract, slides
10:30–11:00 🍵 coffee break
11:00–12:30
  • 11:00 ✨Nicolas Tabareau✨. Not a single proof assistant for all, but proof assistants for everyone (invited talk). slides
  • 12:00 Erik Martin-Dorel, Enrico Tassi. SSReflect in Coq 8.10. abstract, slides, demo
12:30–14:00 🍱 lunch break
14:00–15:30
  • 14:00 Kazuhiko Sakaguchi. Validating Mathematical Structures. abstract, slides, demo
  • 14:30 Florian Steinberg. Some formal proofs about summable sequences in Coq. abstract
  • 14:50 🐓Coq development team🐓. Discussion session. slides
15:30-16:00 🍵 coffee break
16:00–17:30
  • 16:00 Christian Doczkal, Damien Pous. Graph Theory in Coq: Minors, Treewidth, and Isomorphisms. abstract
  • 16:30 Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka. Experience Report: Type-Driven Development of Certified Tree Algorithms in Coq. abstract, slides
  • 17:00 Bruno Bernardo, Raphaël Cauderlier, Basile Pesin, Zhenlei Hu, Julien Tesson. Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts. abstract, slides

Invited Talk

  • Nicolas Tabareau: Not a single proof assistant for all, but proof assistants for everyone.

    Abstract:

    The desiderata of users of proof assistants are very disparate. Classical Logic, univalence, axiom of Choice, exceptions. Then can even be incompatible (univalence + UIP). However, the development of a usable/fast/reliable proof assistant is an enormous engineering task. So it is not conceivable to develop a new proof assistant for each kind of use.

    In this talk, we will present a possible way to provide domain-specific proof assistants using Coq. The key ingredients are the definition of syntactic translations to justify richer theories by compilation to simpler theories and the use of rewrite rules (as available now in Agda) to implement a usable richer theory directly inside Coq using computational axioms.

Accepted Talks

  1. Kazuhiko Sakaguchi. Validating Mathematical Structures
  2. Akira Tanaka. A Gallina Subset for C Extraction of Non-structural Recursion
  3. Christian Doczkal and Damien Pous. Graph Theory in Coq: Minors, Treewidth, and Isomorphisms
  4. Bruno Bernardo, Raphaël Cauderlier, Basile Pesin, Zhenlei Hu and Julien Tesson. Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts
  5. Reynald Affeldt, Jacques Garrigue, Xuanrui Qi and Kazunari Tanaka. Experience Report: Type-Driven Development of Certified Tree Algorithms in Coq
  6. Erik Martin-Dorel and Enrico Tassi. SSReflect in Coq 8.10
  7. Matthieu Sozeau, Yannick Forster, Simon Boulier, Nicolas Tabareau and Théo Winterhalter. Coq Coq Codet!
  8. Florian Steinberg and Holger Thies. Computable analysis, exact real arithmetic and analytic functions in Coq
  9. Florian Steinberg. Some formal proofs about summable sequences in Coq

Registration

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

Important Dates

June 10 2019
Deadline for abstract submission (Extended)
July 2 2019
Notification to authors
July 23 2019
Final version of the accepted abstracts
September 8 2019
Workshop

Submission Instructions

Authors should submit short proposals through EasyChair.

Format

Extended abstract:

  • PDF
  • less than 2 pages
  • full-page style
  • single-column

Topics

Relevant subject matter includes but is not limited to:

  • Theory and implementation of the Calculus of Inductive Constructions
  • Language or tactic features
  • Plugins and libraries for Coq
  • Techniques for formalization programming languages and mathematics
  • Applications and experience in education and industry
  • Tools and platforms built on Coq (including interfaces)
  • Formalization tricks and pearls

Organization

Program Committee

Contact (co-chairs)

reynald.affeldt AT aist.go.jp, garrigue AT math.nagoya-u.ac.jp

Previous Coq Workshops