Pierre Letouzey edited this page Oct 12, 2017 · 39 revisions

The Coq development working groups

Organization

  • As of November 2013, it has been decided to have working groups every two months (Summer excepted) in Paris, at the Sophie Germain building. They are announced 1 month and a half in advance.

    The next Coq Working Group

  • It has also been decided to have a bug session ruling on pull requests and recent bugs every two months (Summer excepted).

Latest Coq WG's, ADT meetings and Users/Developers meetings (in inverse chronological order)

Past roadmap for version 8.4

  • new proof engine with existential variables instantiable by tactics, and, hopefully structured proof scripts (Arnaud Spiwack)
  • native support for eta-conversion (Hugo Herbelin) and maybe axiom K
  • new comprehensive abstract library of numbers, specifying standard arithmetical operations (including power, square root, log, ...) and standard bitwise operations (shift, logical and, or, xor, ...) (Pierre Letouzey, carrying on preliminary works from Evgeny Makarov, also using material from Laurent Théry and Benjamin Grégoire)
  • new model of communication, process based instead of thread based, between Coq and CoqIDE, allowing multi-sessions and interruptability of Coq

Roadmap for version 8.5

  • improved support for pattern-matching on inductive subfamilies à la Agda (see also the Equations plugin)
  • native support for machine word arithmetic and arrays (see Benjamin Grégoire and Maxime Dénès' native branch)
  • applications of the new proof engine: multi-goals tactics? deep backtracking? (Arnaud Spiwack)
  • binding the libraries of Peano numbers and rational numbers to the Numbers architecture
  • asynchronous interaction (parallel compilation of proof scripts, modular compilation of files)
  • miscellaneous tactic improvements (rewriting strategies, improved induction tactics, ...)
  • improvements of the guard condition
  • full universe polymorphism
  • optimized representation of records with native projections
  • a new infrastructure for user contributions
  • a reworking of coqdoc (François Ripault)

The future of Coq

In the longer term, we plan to investigate

  • foundations of the Calculus of Inductive Constructions
    • how to support some form of extensional reasoning? (see the CoqMT prototype for native support of decidably true equations over natural numbers)
    • support for proof-irrelevance in the conversion (either by reasoning in Miquel-Barras-Bernardo's Implicit Calculus of Inductive Constructions or by following Werner's approach)
    • support for K at the Set level
    • induction-recursion
    • compatibility of the logic with the univalent homotopy model
  • a library of mathematical structures (see also discussion page)
  • a typed tactic language (Yann Régis-Gianas, Lourdes del Carmen González Huesca, Guillaume Claret)
  • a cleaning phase of the tactics
  • more solid foundations for the different forms of unification used in Coq (for proving and for type inference)
  • graphical user interfaces: JEdit-based interfaces (see Paral-ITP project), design of a Coq-GUI communication protocol, miscellaneous extensions of CoqIDE (wish list)

Under consideration are

  • aspects of the ssreflect tactic language
  • proof generation from the alt-ergo theorem prover
  • kernel-embedded decision procedures (see the CoqMT prototype for natively solving quantifier-free arithmetic)
  • full universe polymorphism

Miscellaneous

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.