Home

The Coq Workshop 2016

The 8th Coq Workshop


Nancy, France
August 26, 2016
(A satellite workshop of ITP 2016)

The Coq Workshop series brings together Coq users, developers, and contributors. While conferences like ITP 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.

Submission Instructions

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. Relevant subject matter includes but is not limited to:

  • Language or tactic features
  • Theory and implementation of the Calculus of Inductive Constructions
  • Applications and experience in education and industry
  • Tools and platforms built on Coq
  • Plugins and libraries for Coq
  • Interfacing with Coq
  • Formalization tricks and Coq pearls

Invited Talks

Michael Soegtrop. Towards Industrial Application of Coq - Why and How
Abstract: In the past, formal verification has mostly been done with highly specialized tools in isolated islands. The CompCert Compiler by Xavier Leroy et al. together with the VST C toolchain and its applications in cryptography by Andrew W. Appel et al. have shown that INRIA Coq is powerful and flexible enough to connect formalizations from different areas and levels of abstraction. The steadily increasing pace in system complexity and the resulting multi-billion dollar system development cost, require new methods of collaboration. The machine verified combination of modules to a complex system, as done in the NSF deepspec project, is a promising way to further increase development speed and to reduce costs. The way ahead is still a steep and stony one, but it is made increasingly accessible, especially by educational efforts. There are, however, still some missing pieces.
H. Herbelin and M. Sozeau. Coq Development
Abstract: We will present the history and recent and envisioned developments of the Coq system, including the new 8.5 and 8.6 versions. We will also focus on current efforts in the organization of the development and the community. This session will be an occasion to have a discussion with users on the features and directions taken by the system. Finally we will give an overview of projects worldwide around Coq.

Contributed Talks

Rieuwert Blok and Corneliu Hoffman. SpatchCoq
Abstract: This is a project on the use of Coq to assist mathematics students in writing structured proofs, by means of an interface between natural language and Coq. The tool we develop also allows exporting proofs to LaTeX and, in time, we hope it will develop into a platform involving complementary mathematical tools such as Sage and GAP. Thus, we aim to contribute to bridging the gap between computer scientists developing proof assistants and mathematics students and researchers using Coq as a standard tool for writing proofs. We would like to demonstrate this tool during the workshop and invite informal discussion and suggestions from the Coq community.
Thomas Tuerk and Fireeye Formal Methods Team Dresden. Efficiently Executable Sets used by FireEye
Abstract: FireEye provides cybersecurity solutions for detecting, preventing and resolving cyber-attacks. In order to increase the confidence in many of our products we perform proofs of security-critical software components in parallel with development of the components themselves. We carry out the proofs in a Coq model that follows the structure of the implementation, but is much more abstract. The resulting gap is bridged by model-based testing. Our testing framework is developed in OCaml and hinges on Coq's code extraction to obtain an executable version of the model. We execute millions of test cases, each with a state comprising thousands of objects. Thus, performance is a critical aspect: we need to fine-tune the used data structures based on the frequency of the operations performed. Coq's sets library, while well-suited for mathematical reasoning, proved to be a bottleneck for our testing framework. In this note, we describe an extension of this library that drastically improves its usefulness in our development.
Lionel Rieg. Formalizing extensible languages in Coq
Abstract: This talk presents a technique for formalizing a programming language with on-the-fly extensions, meaning that one can add new constructions in the language at any time. An example case study is given: Krivine's classical realizability.
Yannick Forster and Fabian Kunze. Verified Extraction from Coq to a Lambda-Calculus
Abstract: We present a framework to export programs written in Coq to a weak call-by-value lambda calculus. The calculus can be seen as a very basic functional programming language, featuring abstraction, match-constructs based on Scott's encoding and full recursion. The extraction from Coq is not verified itself, but produces proofs for the correctness of each single extracted program semi-automatically. The frameworks builds on the Coq plugin Template Coq by Gregory Malecha. It eliminates the non-computational parts of the Gallina program and produces a lambda-term and the corresponding correctness statement, which in turn can be verified using several provided automation tactics.
Yves Bertot. Arithmetic Geometric Means and the computation of PI
Abstract: I propose to describe a mathematical formalization in analysis that leads to an algorithm able to compute up to a million decimals of PI inside the Coq system.
Benjamin Gregoire and Enrico Tassi. Boolean reflection via type classes
Abstract: The SSReflect proof language provides the view mechanism to switch from the computational realm of bool to the semantic one of Prop. To minimize the syntactic noise due to view application SSReflect accepts views as annotations of most linguistic constructs. Still a user needs to mention the view name explicitly, even when there is only one view to be applied. We propose a type-class based machinery to attach canonical views to predicates and connectives to relief the Coq user from some of the bookkeeping required by the boolean reflection formalization technique.

Schedule

Submission

Authors should submit short proposals through EasyChair. Submissions should be in portable document format (PDF). Proposals should not exceed 2 pages in length in single-column full-page style.

This year, we are open to many ideas on how to use the workshop time. Some suggestions to drive proposals include sessions on tool demonstrations or lessons learned from teaching Coq.

Important Dates

  • June 1: Deadline for proposal submission
  • June 15: Acceptance notification
  • August 26: Workshop in Nancy

Submission URL

https://www.easychair.org/conferences/?conf=coq8

Program Committee

Organization

Contacts: magaud@unistra.fr and narboux@unistra.fr