**Karl Palmskog @palmskog** posted in **CoqHammer 1.2.1 for Coq 8.10 and 8.11**

We are happy to announce the release of CoqHammer 1.2.1 for Coq 8.10 and Coq 8.11.

These releases include new automated reasoning tactics based on a general proof search procedure for the Calculus of Inductive Constructions, as described in a paper to appear in the proceedings of IJCAR 2020. The procedure is shown to be superior to many other general procedures, such as Coq’s firstorder tactic, o...

**@affeldt** posted in **MathComp 1.11.0 released**

We are proud to announce the immediate availability of the

Mathematical Components library version 1.11.0.

This release is compatible with Coq 8.7, 8.8, 8.9, 8.10, 8.11.

The main improvement introduced by this release is the introduction of

order structures. The change should mostly be visible by users of ssrnum.

Version 1.11.0 fixes a problem of 1.11+beta1 so that we allow again

min and max...

**Guillaume Melquiond @silene** posted in **CoqInterval 4.0 released**

The CoqInterval library provides tactics for simplifying the proofs of inequalities on expressions of real numbers, for Coq 8.8 and later. See http://coq-interval.gforge.inria.fr/ for the documentation. As usual, it is available as the coq-interval Opam package.

Since this release comes with some major breaking changes, I am exceptionally announcing it here to help users with the transition.

Ove...

**Clément Pit-Claudel @cpitclaudel** posted in **First release of Kôika 🦑, a core language for rule-based hardware design**

Hi all,

In preparation for PLDI, Thomas Bourgeat and I recently made our first public release of Kôika, a Coq EDSL for rule-based hardware design. Here is a brief description, taken from the README:Kôika is an experimental hardware design language inspired by BlueSpec SystemVerilog. Kôika programs are built from rules, small bits of hardware that operate concurrently to compute state updates ...

These were the last 4 announcements on Discourse. Starting now, anyone wanting to announce a new release or event may do so on Discourse only and it will be forwarded to Zulip. This stream is otherwise restricted (only admins can post here). So if you wish to post a reply to an announcement, head over to Discourse (note that replies won't be forwarded to Zulip).

**Pierre Marie Pédrot @ppedrot** posted in **Coq 8.11.2**

Coq 8.11.2 is now officially released! As usual, you’ll find it on

or in your favourite packaging infrastructure.

Coq 8.11.2 brings in a handful of minor bugfixes, see the changelog at

https://coq.github.io/doc/V8.11.2/refman/changes.html#changes-in-8-11-2

**Théo Zimmermann @Zimmi48** posted in **First beta release of Coq 8.12 (and a call for help to improve the documentation)**

We are happy to announce the first beta release of Coq 8.12.

This new version integrates many usability improvements, in particular to notations, scopes and implicit arguments, along with many bug fixes and major improvements to the reference manual. See the changelog for details.

As usual, we are looking for feedback from beta testers. In addition, we are looking for beta readers of the update...

**Matthieu Sozeau @mattam82** posted in **Equations 1.2.2 for Coq 8.11 and Coq 8.12**

It is my pleasure to announce the release of Equations 1.2.2 for Coq 8.11 and Coq 8.12. Equations 1.2.2 is a bugfix release of the 1.2 version solving a number of issues detailed in the release notes, notably on the dependent elimination and induction tactics. It is compatible with Coq 8.12 beta1 (package coq-equations.1.2.2+8.12 in the coq-opam core-dev repository).

Enjoy!

**Théo Zimmermann @Zimmi48** posted in **Call for partipation to the Coq workshop 2020**

July 5-6, the Internet.

https://coq-workshop.gitlab.io/2020/

The Coq Workshop 2020 is part of IJCAR 2020 and the Paris Nord Summer of LoVe 2020.

Registration is free of charge, but required: https://fscd-ijcar-2020.org/register

The Coq workshop 2020 is the 11th Coq Workshop. The Coq Workshop series brings together Coq users, developers, and contributors. While conferences usually provide a v...

**@Guest0x0** posted in **[ANN] Coqoune**

I am glad to announce the first public release of coqoune, a Coq plugin for the kakoune editor, featuring a similar interface to coqIDE.

The features provided by coqoune is currently rather primitive, compared to more mature Coq environments like coqIDE, vsCoq, etc. The benefits of coqoune is basically those of the kakoune editor, for example:kakoune features a great modal editing interface a...

**Karl Palmskog @palmskog** posted in **Initial release of Roosterize, a tool for suggesting lemma names, for Coq 8.10**

Dear Coq users and developers,

We are happy to announce the initial release of Roosterize, a tool for suggesting lemma names in Coq verification projects.Roosterize learns and suggests lemma names using neural networks that take serialized Coq lemma statements and elaborated terms as input. The technique is described in a research paper published in the proceedings of IJCAR 2020, where it was...

**Karl Palmskog @palmskog** posted in **Initial release of machine learning dataset based on Mathematical Components 1.9.0**

Dear Coq users and developers,

We are happy to announce the initial release of a dataset for use in machine learning, based on Coq 8.10.2 and the Mathematical Components library version 1.9.0.The dataset is based on 449 source files from 21 Coq projects, which are in total over 297k lines of code and contains over 23k lemmas, with projects divided into tiers based on adherence to the MathComp...

**Clément Pit-Claudel @cpitclaudel** posted in **PLV has a new blog!**

Hi all,

We just launched our new blog at https://plv.csail.mit.edu/blog/! Multiple members of our lab were looking for an informal way to share research updates, Coq tips, tutorials, and new ideas, so we set one up.

We’re launching with a few posts already, plus a small intro page at https://plv.csail.mit.edu/blog/pages/how-to.html:Some Coq tips:

How to write a type-safe unwrap (aka fromJ...

**@RalfJ** posted in **Iris 3.3 and std++ 1.4**

Hello everyone,

We are pleased to announce the release of Iris 3.3, a concurrent separation logic framework for Coq. For an overview of the numerous research projects employing Iris, see https://iris-project.org/. Iris 3.3 is accompanied by std++ 1.4, an extended “standard” library for Coq.

This Iris release does not have any outstanding highlights, but contains a large number of improvements al...

**Li-yao Xia @Lyxia** posted in **Coq Planet, a link aggregator about Coq**

There are so many sites to talk about Coq nowadays. You can now find many recent discussion threads in one place at https://coq.pl-a.net

**Théo Zimmermann @Zimmi48** posted in **Coq 8.12.0 is out!**

Dear Coq users,

We are happy to announce the release of Coq 8.12.0.

Some highlights from this release are:

- a new binder notation for non-maximal implicit arguments;
- an improved Search command which accepts more complex queries;
- many additions to the standard library;
- a restructured reference manual;
- the deprecation of the omega tactic in favor the lia tactic.

Please see the chang...

**@Sophie_Tourret** posted in **CADE-28 Call for Papers, Workshops, Tutorials, and Competitions**

CADE-28: Call for Papers, Workshops, Tutorials and Competitions

The 28th International Conference on Automated Deduction (CADE-28)

Carnegie Mellon University, Pittsburgh, USA. 11-16th July 2021.

http://www.cade-28.info

CADE will carefully monitor the development of the COVID-19 pandemic, and take

guidance from from the health authorities, to determine whether CADE-28 will be

physical or onl...

**Pierre Marie Pédrot @ppedrot** posted in **[poll] Next CUDW 2020 -- Reloaded**

as you may recall the Coq User and Developer Workshop that was supposed to take place in June was cancelled. Since it is a very helpful event for people trying to get into the intricacies of the Coq development, we are tentatively trying to get an ersatz version of the CUDW this fall.

The exact format is not decided yet, but the event will be held remotely and spread over a week. In order to sett...

**@amintimany** posted in **CoqPL 2021: Call for Presentations**

===================================================================

CoqPL 2021`7th International Workshop on Coq for Programming Languages -- January 19, 2021, co-located with POPL Copenhagen, Denmark CALL FOR PRESENTATIONS https://popl21.sigplan.org/home/CoqPL-2021`

====...

**Matthieu Sozeau @mattam82** posted in **PhD Position on Certified Extraction in Nantes**

The Gallinette team is looking for a highly qualified PhD student to

work on an Inria-Nomadic Labs project on the subject of certified

extraction from Coq to OCaml. The student will be part of the Gallinette

team in Nantes, attached to the Inria Rennes - Bretagne Atlantique

research center (http://gallinette.inria.fr). The thesis will be funded

for 3 years, and the starting date is flexible b...

**Jonathan Protzenko @msprotz** posted in **Call for Presentations: PriSC 2021 @ POPL 2021 **

All details are on the PriSC site

https://popl21.sigplan.org/home/prisc-2021 and in this email.

Call for Presentations: PriSC 2021 @ POPL 2021

The emerging field of secure compilation aims to preserve security properties of programs when they have been compiled to low-level languages such as assembly, where high-level abstractions don’t exist,

and unsafe, unexpected interactions with libraries,...

**Mariano M. Moscato @marianomoscato** posted in **NASA Formal Methods 2021 - Call for Papers**

(Apologies for possible cross-posting.)

The Thirteenth NASA Formal Methods Symposiumhttps://shemesh.larc.nasa.gov/nfm2021/

24-28 May 2021

Norfolk, VA, USAThe symposium will be held in an in-person/virtual hybrid format in Norfolk, VA, USA, possibly transitioning to fully virtual depending on the COVID-19 situation.

Theme of the Symposium

The widespread use and increasing complexity of miss...

**Donald Sebastian Leung @DonaldKellett** posted in **Coq 8.12 is now supported on Codewars**

The Codewars community is excited to announce the support of Coq 8.12 for all approved Kata (code challenges) and all but 2 Beta Kata as of 08/10/2020. Here at Codewars, we believe that practice makes perfect and in order to ensure the continued quality of our platform as an invaluable training resource for those wishing to learn Coq and/or further refine their Coq-fu, it is necessary to support t...

**Pierre Marie Pédrot @ppedrot** posted in **Next CUDW 2020/11/30 to 2020/12/04 — Save the Date!**

At last, the Coq User and Developer Workshop has been properly scheduled! It will be held remotely between November, 30th and December, 4th. Given the novelty of this endeavour, the precise organization, format, and technology used are yet to be decided.

There is a dedicated Zulip stream to precisely discuss these matters. If you are interested, you are encouraged to join atCrowdsourcing a CU...

**@barryjay** posted in **Tree Calculus**

The draft of my book “Reflective Programs in Tree Calculus” is now available for comment at https://github.com/barry-jay-personal/tree-calculus/blob/master/tree_book.pdf Some front-matter is available from https://github.com/barry-jay-personal/tree-calculus/blob/master/tweets_on_trees.pdf

It may be of interest for two reasons:all proofs have been verified in Coq, and

the subject matter will be...

**@JasonGross** posted in **Ph.D. Defense of Jason Gross on Performance Engineering of Proof-Based Software Systems at Scale**

To those of you who may be interested, I’ll be defending my Ph.D. thesis (titled “Performance Engineering of Proof-Based Software Systems at Scale”, aka “Why is Coq so Slow‽ and How Do We Fix It?”) on Monday, November 30th at 11 am EST on Zoom. Anyone is welcome to attend; email me directly at jgross@mit.edu if you’d like the zoom link and password (not shared here to prevent zoombombing).

Abstr...

**Clément Pit-Claudel @cpitclaudel** posted in **Alectryon: tools for writing technical documents that mix Coq code and prose**

Hi all,

I’ve just released Alectryon 1.0!

Alectryon is a collection of tools for writing technical documents that mix Coq code and prose. It includes a compiler that produces interactive webpages from Coq source files, as well as tools to translate back and forth between Coq and reStructuredText, allowing you to toggle between the proof and prose views of a file at will as you edit it. From the...

**Théo Zimmermann @Zimmi48** posted in **Coq 8.12.1 is out!**

Dear Coq users and contributors,

We are happy to announce the release of Coq 8.12.1.

This release contains numerous bug fixes and documentation improvements. Some bug fix highlights:Polymorphic side-effects inside monomorphic definitions were incorrectly handled as not inlined. This allowed deriving an inconsistency.

Regression in error reporting after SSReflect’s case tactic. A generic error...

**@affeldt** posted in **MathComp 1.12.0 released**

We are proud to announce the immediate availability of the Mathematical

Components library version 1.12.0.

The webpage, and documentation, are available at https://math-comp.github.io/.

This release is compatible with Coq 8.10, Coq 8.11, and Coq 8.12.

The main changes are:

support for Coq 8.7, 8.8, and 8.9 have been dropped,

a change of implementation of intervals and the updated theory,

th...

**@Lasse** posted in **Announcing Tactician 1.0 beta1**

I’d like to announce the first beta release of Tactician, a tactic machine learning plugin for Coq. I have copied the release notes below:

We would like to announce Tactician 1.0 beta1, the first official release of Tactician.

Tactician is a tactic learner and prover for the Coq Proof Assistant. The system will help users make tactical proof decisions while they retain control over the general ...

**Erik Martin Dorel @erikmd** posted in **About the -native-compiler flag and the coq-native opam package (to be released before Coq 8.13+beta1)**

Dear Coq users,

This announcement deals with Coq’s native_compute support (which is typically interesting to get increased performance when using reflexive tactics). It focuses in particular on the -native-compiler flag for both ./configure and coqc binaries, as well as the corresponding packaging in opam-repository.

TL;DR: Following the discussion that took place in the CEP 48 (Coq Enhancement ...

**Enrico Tassi @gares** posted in **Release of Coq 8.13+beta1**

Dear Coq users,

The Coq development team is proud to announce the immediate

availability of Coq 8.13+beta1:The full list of changes is available at the following address

We encourage our users to test this beta release, in particular:

- The windows installer is now based on the Coq platform: This

greatly simplifies its build process and makes it easy to add

more packages. At the sa...

**@lthms** posted in **Towards coqffi.1.0.0 (Call for Testers)**

I am pleased to announce that coqffi is almost ready for its first official release, and is already available in the released repository of the Opam Coq Archive for users to try it.

If you do not already know, coqffi generates the necessary Coq boilerplate to use OCaml functions in a Coq development, and configures the Coq extraction mechanism accordingly. In practice, it greatly reduces the hass...

**Catalin Hritcu @catalin.hritcu** posted in **Research internships at MPI**

3 Max Planck Institutes are offering CS research internships next summer. We are looking for advanced students in all areas of CS. Applicants do not need prior research experience. The application deadlines are December 31 and January 31: https://www.cis.mpg.de/internships

**Théo Zimmermann @Zimmi48** posted in **Coq 8.12.2 is out**

Dear Coq users and contributors,

We are happy to announce the release of version 8.12.2 of the Coq

proof assistant:This release is virtually identical to the 8.12.1 release except for

two fixes of impacting 8.12 regressions.

In addition, the Windows installer is now based on the Coq platform

(https://github.com/coq/platform), like the one of the recently

released 8.13+beta1 version. For ...

**Enrico Tassi @gares** posted in **Release of Coq 8.13.0**

Dear Coq users,

The Coq development team is proud to announce the immediate

availability of Coq 8.13.0:The full list of changes is available at the following address

https://coq.github.io/doc/v8.13/refman/changes.html#version-8-13

Highlights:

Introduction of primitive persistent arrays in the core language,

implemented using imperative persistent arrays.Introduction of definition...

**Cyril Cohen @CohenCyril** posted in **A formal proof of Abel-Ruffini Theorem in Coq**

Dear Coq community,

I am happy to announce that we – Sophie Bernard, Cyril Cohen, Assia Mahoubi and Pierre-Yves Strub – were able to formalize in Coq a proof of Abel-Ruffini Theorem, which states that there are polynomials of degree 5 that are not solvable by radicals, e.g. X^5 - 4X + 2.

Lemma example_not_solvable_by_radicals :

~ solvable_by_radical_poly ('X^5 - 4%:R *: 'X + 2%:Q%:P).This is...

**Christian Doczkal @chdoc** posted in **[CFP] The Coq Workshop 2021 : Call for Talk Proposals**

The Coq Workshop 2021: Call for Talk Proposals

Colocated with the 12th conference on Interactive Theorem Proving (ITP 2021)

Online

Find this call online at: The Coq Workshop 2021

We are pleased to invite you to submit talk proposals for the Coq

Workshop 2021, which will be held online on July 2nd, 2021.

The Coq Workshop is part of ITP 2021, which will also be held online.

The Coq Workshop 2...

**Pierre Castéran @casteran** posted in **Hydra battles**

Dear Coq users,

The objective of coq-community <coq-community · GitHub> is to maintain and/or document coq developments. The project hydra-battles (in reference to Kirby and Paris's work) is an attempt to understand which kind of document may go with Coq libraries. It is developped in <GitHub - coq-community/hydra-battles: Variations on Kirby & Paris' hydra battles and other entertaining math in ...

**Enrico Tassi @gares** posted in **[Coq-Club] Release of Coq 8.13.1**

Dear Coq users,

The Coq development team is proud to announce the immediate

availability of Coq 8.13.1:Highlights:

- Fix arities of VM opcodes for some floating-point operations that

could cause memory corruption.

Best,

**Enrico Tassi @gares** posted in **Release of the Coq platform 2021.02.0**

Dear Coq community,

the Coq development team is proud to announce the immediate

availability of the Coq Platform version 2021.02.0

The Coq platform is a distribution of the Coq proof assistant together

with a selection of Coq libraries. It provides a set of scripts to

compile and install OPAM, Coq, Coq libraries and Coq plugins on MacOS,

Windows and many Linux distributions in a reliable w...

**Arthur Azevedo de Amorim @arthuraa** posted in **Deriving: a library for deriving class instances for inductive types**

Hi everyone,

I would like to announce the release of Deriving v0.1.0 (GitHub - arthuraa/deriving: Class instances for Coq inductive types with little boilerplate, available as coq-deriving on OPAM). It is a library for automating the generation of MathComp class instances for inductive types, akin to how deriving declarations work in OCaml or Haskell. With a few lines of code, you can derive inst...

**Fabian Kunze @fakusb** posted in **Release of VSCoq 0.3.4 IDE**

We’d like to announce the most recent release of VSCoq 0.3.4, the extension adding Coq support to the Visual Studio Code IDE.

The new version fixes several usability bugs (unreadable narrow proof views, bad performance in huge files of over 3000 lines and some other glitches that were only fixed by restarting) and improves several other aspects, see changelog.

We of course still have all the oth...

**Matthieu Sozeau @mattam82** posted in **Equations 1.2.4 release**

I am happy to announce availability of equations 1.2.4, a bugfix release that improves the compatibility of equations with ssreflect’s tactics and has more robust automated proofs of the elimination principle associated to a definition, including when functional extensionality is disabled. This version is available on opam for Coq 8.13, 8.12 and 8.11 and should be entirely backwards compatible.

P...

**Guillaume Melquiond @silene** posted in **Interval 4.2, now with plotting**

The 4.2.0 release of Interval departs a bit from the previous versions in that it is no longer just about proving properties of real-valued expressions. It can now be used to investigate such properties visually, that is, it can now plot function graphs from inside Coq. The main difference with traditional computer algebra systems is that a plot is not a list of points obtained by sampling, it is ...

**@Maximilian_Haslbeck** posted in **Proof Ground 2021 - Call for Problems**

Dear Coq enthusiasts,

we are organizing another edition of the proving competition workshop

"Proof Ground", which will take place virtually just before ITP 2021.

Please take noteof our Call for Problems, and spread the word!

**Théo Zimmermann @Zimmi48** posted in **Renaming Coq**

Dear members of the Coq community,

The Coq development team acknowledges the recent discussions (started on the Coq-Club mailing list) around Coq’s logo and name.

We wish to thank everyone that participated in these discussions. Testimonies from people who experienced harassment or awkward situations, reports about students (notably women) who ended up not learning / using Coq because of its nam...

**@Danil_Annenkov** posted in **Certified Elm web apps**

Dear Coq community,

I would like to share a project related to the Elm functional programming language.

As part of ConCert (https://github.com/AU-COBRA/ConCert), we have developed an extraction pipeline that allows for generating Elm code.

We have several simple examples/tests here https://github.com/AU-COBRA/ConCert/blob/master/extraction/examples/ElmExtractExamples.v.

A more “domain-specific...

**Enrico Tassi @gares** posted in **Release of the Coq platform 2021.02.1 - Coq 8.13.2**

Dear Coq community,

the Coq development team is proud to announce the immediate

availability of the Coq Platform version 2021.02.1, based on Coq

8.13.2.

The Coq platform is a distribution of the Coq proof assistant together

with a selection of Coq libraries. See [1] for the project homepage,

and [2] for the new instructions for getting Coq.

For expert users it provides a set of scripts to...

**Christian Doczkal @chdoc** posted in **[CFP] The Coq Workshop 2021 : 2nd Call for Talk Proposals**

The Coq Workshop 2021: 2nd Call for Talk Proposals

Colocated with the 12th conference on Interactive Theorem Proving (ITP 2021)

Online

Find this call online at: The Coq Workshop 2021

We are pleased to invite you to submit talk proposals for the Coq

Workshop 2021, which will be held online on July 2nd, 2021.

The Coq Workshop is part of ITP 2021, which will also be held online.

The Coq Worksh...

**Matthieu Sozeau @mattam82** posted in **Equations 1.3 beta release**

Dear Coq/Equations users, I’m happy to announce version 1.3 of the Equations package.

This is a new major release of Equations, working with Coq 8.13. This version adds an improved syntax (less ; -separation), integration with the Coq-HoTT library and numerous bug fixes. See the reference manual for details.

This version introduces some minor potentially breaking changes along with the following...

**@benediktahrens** posted in **PhD position in HoTT/UF at TU Delft**

A PhD position [1] is open in the Programming Languages group [2] at TU Delft, in the area of HoTT/UF. The student will be supervised by Benedikt Ahrens [3].

Information about the position is available on the dedicated website [1]. If you have any questions or consider applying, please get in touch with Benedikt (benedikt.ahrens@gmail.com).

[1] PhD studentship in homotopy type theory and univale...

**Maximilian Haslbeck @maxhaslbeck** posted in **Proof Ground 2021 - Call for Participation**

Call for participation

Proof Ground 2021

Interactive Proving Contest

June 28, 2021

https://www21.in.tum.de/~wimmers/proofground/

at ITP 2021

Interactive Theorem Proving

June 29 - July 2, 2021, (originally in) Rome, Italy, now fully virtual

https://easyconferences.eu/itp2021/

------------...

**Christian Doczkal @chdoc** posted in **[Call for Participation] July 2nd: The Coq Workshop 2021**

The Coq Workshop 2021: Call for Participation (July 2nd)

Colocated with the 12th conference on Interactive Theorem Proving (ITP 2021)

Online

We are pleased to invite you to participate in the Coq workshop 2021, which will be held online on July 2nd. The Coq workshop is part of ITP 2021.

The Coq Workshop 2021 is the 12th iteration of the Coq Workshop series. The workshop brings together users,...

**@amintimany** posted in **CoqPL 2022: Call for Presentations**

===================================================================

CoqPL 2022`8th International Workshop on Coq for Programming Languages -- January, 2022, co-located with POPL Philadelphia, Pennsylvania, United States CALL FOR PRESENTATIONS https://popl22.sigplan.org/home/CoqPL-20...`

**@jespercockx** posted in **Call for Contributions: WITS 2022**

CALL FOR CONTRIBUTIONS

`1st Workshop on the Implementation of Type Systems WITS 2022 January 22, 2022 Philadelphia, PA, USA https://popl22.sigplan.org/home/wits-2022`

WITS 2022 is the first Workshop on the Implementation of Type

Systems. The workshop will be held on January 22, 2022, in

Phi...

**Théo Zimmermann @Zimmi48** posted in **Call to participate to the WG that will prepare the Coq community survey**

Dear all,

We are about to launch a community-wide survey to get input from the

Coq community and learn more about it. The survey will include things

like demographics, questions about pain points, the roadmap and a

possible renaming.

To prepare this survey, we are setting up a working group. We expect

this working group to coordinate on Zulip and to meet every week for

the next few weeks un...

**Marco Maggesi @maggesi** posted in **School on Univalent Mathematics, Cortona (Italy), July 17-23, 2022**

We are pleased to announce the

School on Univalent Mathematics 2022,

to be held at the Palazzone di Cortona,

Cortona, Italy, July 17-23, 2022Overview

Homotopy Type Theory is an emerging field of mathematics that studies a fruitful relationship between homotopy theory and (dependent) type theory. This relation plays a crucial role in Voevodsky’s program of Univalent Foundations, a new approac...

**Emilio Jesús Gallego Arias @ejgallego** posted in **[ANN] PyCoq preview release**

Dear Coq users and developers,

we are happy to announce the initial release of pyCoq, a Python library to interact with Coq programmatically.The library is very experimental at the moment; expect significant non-backward compatible changes and problems.

We are however doing an early-stage announcement due to:we feel there is significant demand for this kind of library

we’d love to gather ...

**Christian Doczkal @chdoc** posted in **MathComp 1.13.0 released**

We are proud to announce the immediate availability of the Mathematical

Components library version 1.13.0.

The webpage, and documentation, are available at

https://math-comp.github.io/.

This release is compatible with Coq 8.11, 8.12, 8.13 and 8.14.

The main changes are new theories on the diagonalization of matrices,

on bounded sequences, and on the pairwise predicate.

The contributors to t...

**Tiago Cogumbreiro @AssertionError** posted in **Turing: a library to teach Introduction to Theory of Computation**

The Turing project aims to offer the foundations of a course on introduction to the theory of computing. We are formalizing some content of the textbook Introduction to the Theory of Computation, by Michael Sipser.

Our library includes results on

Formal languages: common operators and language equality results

Regular languages: regular expressions, pumping lemma

Turing machines: acceptance, ...

**Tej Chajed @tchajed** posted in **Iris 3.5 and std++ 1.6 released**

We are happy to announce the release of Iris 3.5 and std++ 1.6. Iris is a concurrent separation logic framework for Coq; for an overview of the numerous research projects employing Iris, see https://iris-project.org/. std++ is an extended “standard” library for Coq.

The highlights and most notable changes of Iris 3.5 are:Coq 8.14 is now supported, while Coq 8.12 and Coq 8.13 remain supported.

T...

**Théo Zimmermann @Zimmi48** posted in **Coq Platform 2021.09.0**

Dear Coq community,

On behalf of the Coq development team, the release managers of

Coq 8.13 and Coq 8.14, and the Coq Platform team, we are happy to

announce the immediate availability of the Coq Platform version

2021.09.0.

This is the first Coq Platform release which includes several

versions of Coq. Furthermore, the included package set was

significantly extended since the 2021.02.2 relea...

**Jim Fehrle @jfehrle** posted in **Preview of Ltac Visual Debugger in CoqIDE is now available**

Today’s release of Coq Platform 2021.09.0 includes a preview of the Ltac Visual Debugger on top of Coq 8.14. It’s not merely “interactive”; it’s a visual debugger. It’s described in https://github.com/coq/coq/wiki/Ltac-Debugger-Preview. Let me know your suggestions for it and whether you find it useful.

[image.png]

**Emilio Jesús Gallego Arias @ejgallego** posted in **Coq Hackaton Winter 2022 edition**

Dear all,

We are happy to announce a virtual Coq Hackathon and Working Group on Feb 15th-17th 2022. We were hoping to make this event a hybrid one, but due to the current circumstances it will be online only.

The event is targeted at people who are interested in the implementation of Coq, and would like to learn more about how Coq works and possibly contribute to its development. We hope that th...

**@Cyril_Cohen** posted in **MathComp 1.14.0 released**

We are proud to announce the immediate availability of the Mathematical Components library version 1.14.0.

The webpage, and documentation, are available at https://math-comp.github.io/.

This release is compatible with Coq 8.11, 8.12, 8.13, 8.14 and 8.15.

This release only includes minor changes.

The contributors to this version are: Cyril Cohen, Erik Martin-Dorel, Kazuhiko Sakaguchi, Laurent T...

**Tej Chajed @tchajed** posted in **Iris 3.6 and std++ 1.7 released**

We are happy to announce the release of Iris 3.6 and std++ 1.7. Iris is a concurrent separation logic framework for Coq; for an overview of the numerous research projects employing Iris, see https://iris-project.org/. std++ is an extended “standard” library for Coq.

The highlights and most notable changes of Iris 3.6 are:Coq 8.15 is now supported, while Coq 8.13 and Coq 8.14 remain supported.

...

**Théo Zimmermann @Zimmi48** posted in **Coq Platform 2022.01.0**

Dear Coq community,

On behalf of the Coq development team, the release managers of

Coq 8.14 and Coq 8.15, and the Coq Platform team, we are happy to

announce the immediate availability of the Coq Platform version

2022.01.0.

Release highlights:

- An important newly added package, coq-hammer, provides the hammer

tactic, which uses external ATPs (Automated Theorem Provers) to

automatically cr...

**Théo Zimmermann @Zimmi48** posted in **Coq community survey 2022**

Dear Coq community,

The Coq team requests your participation in the Coq community survey 2022. This survey will help get an updated picture of the Coq community, and help inform future decisions. Participation from every Coq user, learner or prospective user is extremely useful. Please advertise the survey to your students, colleagues, and friends, who are learning or using Coq, but might have mi...

**Enzo Crance @ecranceMERCE** posted in **Trakt 1.0 released**

Hello,

I am glad to announce the first release of Trakt, a generic goal preprocessing tool for proof automation tactics in Coq.Automation tactics in Coq are usually tailored for specific subsets of goals. Yet, when designing their proof statements, Coq users can choose from a range of different inductive types with advantages and drawbacks (computational efficiency, ease of proof, etc). This v...

**Assia Mahboubi @amahboubi** posted in **Workshop: Machine-Checked Mathematics, March 2-4**

Sander Dahmen, Assia Mahboubi, and I have been planning a workshop for a while at the Lorentz Center in Leiden. Pandemic planning is impossible and the workshop keeps changing shape. But we can finally be certain enough to announce: we will be hosting a virtual workshop, Machine-Checked Mathematics, March 2-4! It will happen European afternoons, in an attempt to be accessible by as many people as ...

**Karl Palmskog @palmskog** posted in **The Coq Workshop 2022: Call for Presentation Proposals**

The Coq Workshop 2022: Call for Presentation Proposals

We are pleased to invite you to submit presentation proposals for the Coq Workshop 2022, which will be held in Haifa, Israel on August 12, 2022, as part of FLoC 2022.

The Coq Workshop 2022 is affiliated with ITP 2022, and is the 13th installment of the Coq Workshop series. The workshop brings together users, contributors, and developers of t...

**Talia Ringer @tlringer** posted in **Job opening: visiting research programmer, machine learning for Coq**

Hi all, hope you’re doing well!

I’m hiring a visiting research programmer to build machine learning tools for Coq. This position will mostly be focused on building a usable tool that people can interact with—so some Coq plugin development, some interface design, and some interfacing with machine learning models and frameworks. But the programmer will also be involved in multiple aspects of a cros...

**Théo Zimmermann @Zimmi48** posted in **Proof Assistants SE public beta**

There is now a Stack Exchange Q&A site dedicated to Proof Assistants! Do not hesitate to post and answer Coq questions there (use the coq tag).

**Pierre Marie Pédrot @ppedrot** posted in **Coq 8.16 Release Schedule**

The release schedule for Coq 8.16 has been roughly decided.

The Release Manager will be thy servant, Pierre-Marie Pédrot. Following the release cycle CEP, the first move of the 8.16 will be the official branch out of master, followed by a swift V8.16+rc1 tag. Eventually a V8.16.0 tag will be published when the release process converges.

Tentative schedule:Mid May 2022: 8.16 branch

End of May ...

**Évariste G. @evaristeg** posted in **Upcoming Coq Hackathon and workgroup session**

Hi everyone,

We are organizing an upcoming Coq Hackathon and workgroup session to work on two topics: jsCoq (see the Wiki section here) and the initial implementation of “CoqDB”, an attempt to develop a unified framework where information about Coq objects and metadata can be handled (see the Wiki section here).

At this time, we would like to define the date for this upcoming event. Please use t...

**Évariste G. @evaristeg** posted in **Upcoming Coq Hackathon and workgroup session on Thursday, March 31st**

Hi everyone,

Our next Coq Hackathon and workgroup session is happening this Thursday, March 31st, 14h00 Paris time (08h00 NYC time - 05h00 Seattle time). Please join us! We’ll be focusing on two topics: jsCoq (see the Wiki section here) and the initial implementation of “CoqDB”, an attempt to develop a unified framework where information about Coq objects and metadata can be handled (see the Wiki...

**Ana Borges @ana-borges** posted in **PhD student position on proof theory and verification of legal software in Coq, Barcelona (Deadline: April 3rd, AoE)**

The University of Barcelona offers a 3 year PhD position in collaboration with the Catalan industrial sector. The industrial component of the PhD revolves around the development and verification of legal software in Coq within Formal Vindications SL (formalvindications.com). This work will be complemented with the formalisation of parts of logic/mathematics and possibly research of a less applied ...

**@shinnar** posted in **FormalML: A library for (general) probability**

We would like to announce our (open source and publicly available)

library for working with general probability spaces in Coq. Starting

with Sigma-Algebras, it works its way up to general expectation, and

general conditional expectation (defined over any nonnegative or

finite expectation measurable random variable), with the expected

properties.

This is used for various applications, such a...

**Guillaume Melquiond @silene** posted in **Interval 4.5, now with root finding**

The 4.5.0 release of Interval comes with a new pair of tactics: root and root_intro. Contrarily to the original tactics interval and integral (and their *_intro counterparts), root does not compute a new enclosure by forward interval analysis. Instead, it refines an existing enclosure according to a given equation using Newton’s method.

Let us illustrate the root tactic with the quintic equation x...

**Marco Maggesi @maggesi** posted in **School on Univalent Mathematics, Cortona (Italy), July 17-23: Application deadline 15 April**

We are pleased to announce the

School on Univalent Mathematics 2022,

to be held at the Palazzone di Cortona, Cortona, Italy, July 17-23, 2022Application deadline

15 April 2022Overview

Homotopy Type Theory is an emerging field of mathematics that studies a fruitful relationship between homotopy theory and (dependent) type theory. This relation plays a crucial role in Voevodsky’s program of ...

**Théo Zimmermann @Zimmi48** posted in **Coq Platform release 2022.04.0**

Dear Coq community,

On behalf of the Coq development team, the release manager of Coq

8.15, and the Coq Platform team, we are happy to announce the

immediate availability of the Coq Platform version 2022.04.0.

Release highlights:

- Coq 8.15 is now stable and the default version proposed in the Coq Platform.
- Flocq has been upgraded to major version 4.0.0. Flocq 3 is still

available under t...

**@UlrikBuchholtz** posted in **HoTTEST Summer School July+August 2022**

We’re delighted to announce the HoTTEST Summer School, part of the

Homotopy Type Theory Electronic Seminar Talks, which will take

place online everywhere in the world during the months of July and

August 2022.

The school will run both synchronously and asynchronously. The lectures

will be delivered live (between 2:30-4pm UTC) and paired with various

tutorial sessions run by teaching assistan...

**Alex Gryzlov @alex.gryzlov** posted in **HTT 1.0 released**

Hello,

We would like to to announce the first public release of Hoare Type Theory (HTT), a verification system for reasoning about sequential heap-manipulating programs based on Separation logic. It is available on Github and can be installed via opam.

HTT incorporates Hoare-style specifications via preconditions and postconditions into types. A Hoare type ST P (fun x : A => Q) denotes computati...

**Maxime Dénès @maximedenes** posted in **CompCert receives ACM Software System Award**

After Coq in 2013, CompCert receives the 2021 ACM Software System Award. Congrats to everybody involved!

**@erikmd (Erik Martin Dorel)** posted in **ANN: (docker-coq: Bump to Debian 11) & (docker-coq-action: Remove ocaml_version: "minimal")**

TL;DR: if you use docker-coq images and (install Debian packages manually or use the docker-coq-action with ocaml_version: "minimal"), then you could be impacted by the upgrade planned on next Monday 2022-06-27.

Up to now, all changes done in docker-coq and docker-coq-action repositories have been done with a special focus on backward compatibility.

However, two upcoming changes might impact Do...

**@Marcus_Zibrowius** posted in **Full-time positions in formalized mathematics at Düsseldorf**

Heinrich Heine University Düsseldorf is seeking two full-time postdocs

within the projectADAM: Anticipating the Digital Age of Mathematics,

which is funded by the public foundation Stiftung Innovation in der Hochschullehre. The core aim of

the project is to develop, test and publish online resources that

provide an introduction to formalized mathemati...

**@Zimmi48 (Théo Zimmermann)** posted in **Coq Platform release 2022.04.1**

Dear Coq community,

On behalf of the Coq development team, the release manager of Coq

8.15, and the Coq Platform team, we are happy to announce the

immediate availability of the Coq Platform version 2022.04.1.

Release highlights:

The latest release version of Coq has been updated from 8.15.1 to 8.15.2.

The main supported version is:Coq 8.15.2 with the same package collection as the 202...

**@gares (Enrico Tassi)** posted in **MathComp 1.15.0 released**

We are proud to announce the immediate availability of the Mathematical

Components library version 1.15.0

The webpage, and documentation, are available at

https://math-comp.github.io/.

This release is compatible with Coq 8.13, 8.14, 8.15 and 8.16.

The contributors to this version are: Cyril Cohen, ed-hermoreyes,

Enrico Tassi, Erik Martin-Dorel, Evgenii Moiseenko,

Georges Gonthier, Jonathan ...

**@mattam82 (Matthieu Sozeau)** posted in **MetaCoq 1.0 released**

We are happy to announce release 1.0 of the MetaCoq project for Coq 8.14, 8.15, and 8.16, available both as sources and as opam packages. See the website for a detailed overview of the project, introductory material and related articles and presentations.

MetaCoq integrates Template-Coq, a reification and denotation plugin for Coq terms and global declarations, a Template monad for metaprogrammin...

**@amahboubi (Assia Mahboubi)** posted in **Certified Symbolic-Numeric Computation**

We are pleased to make the following:

First Announcement: on May 22 — May 26, 2023 a workshop on`CERTIFIED AND SYMBOLIC-NUMERIC COMPUTATION`

will take place at ENS de Lyon (Lyon, France).

More information can be found on our website:

https://rtca2023.github.io/pages_Lyon/m2.html

The last twenty years have seen the advent of computer-aided proofs in mathematics and this trend is getting more ...

**@mgbedmar (Mireia González Bedmar)** posted in **FormalV 1.0.0 released**

Formal Vindications S.L. is happy to announce the availability of the FormalV Library version 1.0.0.

The library includes three packages:FV Prim63 to MathComp provides conversions from the Coq primitive integers Uint63 and Sint63 to the MathComp natural and integer numbers nat and int, and vice versa, as well as lemmas to rewrite between their respective operations.

FV Check Range provides tac...

**@blanqui (Frédéric Blanqui)** posted in **EuroProofNet workshop on the development, maintenance, refactoring and search of large libraries of formal proofs**

Dear all,

EuroProofNet is going to organize a workshop on the development, maintenance, refactoring and search of large libraries of formal proofs, on September 23-24, in Tbilisi, Georgia, as part of the Computational Logic Autumn Summit 2022, so in co-location with many other interesting conferences and schools (*). See EuroProofNet Workshop on the development, maintenance, refactoring and searc...

**@palmskog (Karl Palmskog)** posted in **Coq Community Survey 2022 Results: Part I**

Coq Community Survey 2022 Results: Part I

In this post, we give an introduction to the survey and then provide the first part (out of three planned parts) of a result summary. This part is about who is using Coq and in what context.Introduction to the Survey

The Coq Community Survey 2022 was an online public survey conducted during February 2022. Its main goal was to obtain an updated picture ...

**@palmskog (Karl Palmskog)** posted in **Coq Community Survey 2022 Results: Part II**

Coq Community Survey 2022 Results: Part II

This post is the second of three that summarize the results of the Coq Community Survey 2022. Here, we cover how people use Coq, such as their Coq version and IDE choice.

We invite the Coq community to give feedback as replies to this post. In particular, please tell us if the survey questions or plot are unclear in any way.Introduction to the survey

...

**@DonaldKellett (Donald Sebastian Leung)** posted in **Coq 8.15.2 now available on Codewars**

Coq 8.15.2 is now available on Codewars, a community-driven platform featuring code challenges (Kata) for learners of all levels and disciplines. This release includes the base compiler, plus versions of selected packages compatible with Coq Platform 2022.04.1:

Equations

mathcompA list of Coq Kata is available through the Kata search page. The original request for Coq 8.15 support can be found...

**@RalfJ** posted in **Iris 4.0 and std++ 1.8 released**

Hi everyone,

We are happy to announce the release of Iris 4.0 and std++ 1.8. Iris is a concurrent separation logic framework for Coq; for an overview of the numerous research projects employing Iris, see https://iris-project.org/. std++ is an extended “standard” library for Coq.

The highlight of Iris 4.0 is the later credits mechanism, which provides a new way to eliminate later modalities.

Thi...

**@gares (Enrico Tassi)** posted in **MathComp Workshop and Winter School (Dec 5-9 2022)**

Dear Coq enthusiasts,

we are organizing a winter school titled

“The Mathematical Components library”

in Sophia-Antipolis (Nice) from Monday 5th December 2022 to Friday

9th. On Wednesday of the same week we are organizing the workshop

“Mathematical Components - 10 years after the Odd Order Theorem”

The school will be in English and will target master or PhD students

with basic knowle...

**@palmskog (Karl Palmskog)** posted in **Coq Community Survey 2022 Results: Part III**

Coq Community Survey 2022 Results: Part III

This is the third post summarizing the results of the Coq Community Survey 2022. It covers Coq features, tools, plugins and libraries and their respective popularity. The first part focused on who respondents are, while the second part focused on how they use Coq.

We invite the Coq community to give feedback as replies to this post. In particular, plea...

**@Benjamin_Pierce** posted in **New release of Software Foundations**

The Software Foundations team is delighted to announce a new release of the entire SF series.

Software Foundations is a set of textbooks on logic, programming language theory, functional algorithms, and machine-assisted proofs of functional and imperative programs, all 100% formalized and machine-checked in Coq. This release brings all volumes up to date with the current release of Coq (8.15.2) a...

**@palmskog (Karl Palmskog)** posted in **Volunteer interim maintainers needed for VsCoq**

The Coq core team and Coq-community are looking for volunteer interim maintainers of the VsCoq project.

VsCoq is an extension of the Visual Studio Code (VS Code) editor to support Coq source files and interaction with Coq. In a recent survey of Coq users, around one third of respondents reported that they use VS Code for Coq.

As described in the public roadmap, VsCoq developers are currently foc...

**@amahboubi (Assia Mahboubi)** posted in **Two positions at the University of Bonn in the field of formal mathematics and computer assisted theorem proving**

See University of Bonn, Hausdorff Center for Mathematics

The cluster of excellence Hausdorff Center for Mathematics (HCM) at the University of Bonn brings together researchers in mathematics and its applications. In this framework the center is looking forward to filling in the area of theoretical mathematics

a permanent W2-Professorship and

a temporary W2-Professorship for five years

in the f...

**@Zimmi48 (Théo Zimmermann)** posted in **Coq Platform 2022.09.0 (including beta version for Coq 8.16.0 and a updated and extended package pick)**

Dear Coq community,

On behalf of the Coq development team, the release manager of Coq

8.16, and the Coq Platform team, we are happy to announce the

immediate availability of the Coq Platform 2022.09.0 release.

Release highlights:

The latest version of Coq has been updated from 8.15.2 to 8.16.0,

with a beta package pick.Many new packages have been added. In particular, Itauto,

mathcomp...

**@gares (Enrico Tassi)** posted in **MathComp Workshop and Winter School (Dec 5-9 2022) - second call**

Dear Coq enthusiasts,

we are organizing a winter school titled

“The Mathematical Components library”

in Sophia-Antipolis (Nice) from Monday 5th December 2022 to Friday

9th. On Wednesday of the same week we are organizing the workshop

“Mathematical Components - 10 years after the Odd Order Theorem”

The school will be in English and will target master or PhD students

with basic knowle...

**@spitters (Bas Spitters)** posted in **PhD/postdoc vacancy on the verification of cryptographic protocols at Aarhus University**

We are looking for a strong PhD-candidate at Aarhus University (DK).

( There may be possibilities for a postdoc position. Please contact me

for more information. )

A description of the project can be found below.

deadline 1 November 2022 at 23:59 CET.

https://phd.nat.au.dk/for-applicants/open-calls/november-2022/privacy-preserving-and-software-independent-voting-protocols

The PhD positions i...

**@jasonrute** posted in **Postdoc and Internship positions at IBM Research**

IBM Research is looking for both a post-doc and a summer intern, both to work at the intersection of AI and interactive theorem proving with me and others.

Post-doc position:

Start Jan 2023 (or later if negotiated)

Based in Yorktown Heights, NY, USA

See here for the post-doc position description and application link.

We are looking to make a decision very soon. If you are interested please do b...

**@silene (Guillaume Melquiond)** posted in **Interval 4.6, now with decimal enclosures and floating-point rounding operators**

The 4.6.0 release of Interval comes with two new features.

First, the *_intro tactics as well as their degenerate forms (for tactic-in-term uses) can now represent enclosure bounds using decimal numbers, for extra readability. This feature is enabled by passing the i_decimal option to the tactics.

From Coq Require Import Reals.

From Interval Require Import Tactic.

Open Scope R_scope.Definition...

**@Matafou (Pierre Courtieu)** posted in **ProofGeneral release 4.5**

We are happy to announce the release of Proof General version 4.5.

Proof General is a generic Emacs mode for proof assistants. It can be instantiated for the proof assistant of your choice, and is supplied ready-customized for Coq, PhoX, EasyCrypt, Qrhl-tool.

Website: https://proofgeneral.github.io/

Core maintainers e-mail: proof-general-maintainers@groupes.renater.fr

Proof General includes th...

**@gares (Enrico Tassi)** posted in **MathComp Workshop and Winter School (Dec 5-9 2022) - last call**

Dear Coq enthusiasts,

we are organizing a winter school titled

“The Mathematical Components library”

in Sophia-Antipolis (Nice) from Monday 5th December 2022 to Friday

9th. On Wednesday of the same week we are organizing the workshop

“Mathematical Components - 10 years after the Odd Order Theorem”

The school will be in English and will target master or PhD students

with basic knowle...

**@CohenCyril (Cyril Cohen)** posted in **Job offer - postdoc position in Inria Sophia Antipolis**

We offer a 1-year long postdoc position from March 1st, in the context of the CoREACT french ANR.

All the details are in the following document http://cyrilcohen.fr/CoREACT1.pdf

Note that the application link in the document is not valid yet and should be active by January.

Best wishes

**@dankoi** posted in **Position in software dependability at the French space agency CNES - Toulouse**

Bonjour,

Une poste en assurance de sûreté de fonctionnement du logiciel est ouverte au CNES-Toulouse :N’hésitez pas à postuler si ces sujets vous intéressent.

Cordialement,

Danko ILIK

**@ejgallego (Emilio Jesús Gallego Arias)** posted in **Coq LSP release 0.1.2**

Dear all,

we are happy to announce the release of coq-lsp 0.1.2, a new language Server and VSCode extension for the Coq interactive proof assistant.

coq-lsp aims to provide a modern and streamlined proof-editing experience, supporting incremental checking, markdown documents, and an error recovery strategy friendly to step wise development of proof documents.

The 0.1.2 release has been signific...

**@karthikbhargavan** posted in **Verification Jobs @ Cryspen (France/Germany)**

Cryspen is a small research-oriented company that seeks to apply formal verification tools to build high-assurance production-ready cryptographic software. We have a few open roles at Cryspen right now in Germany and in France.

In particular, we are looking to hire a Software Verification Engineer who will focus on implementing and verifying high-assurance software, which includes writing and mai...

**@lthery (Laurent Théry)** posted in **VsCoq 0.3.7 is out**

Vscoq 0.3.7 is out!!

Change log :0.3.7

add an option to disable “Proof View Diff” (#321 by @Blaisorblade)

add logo as icon to coq file (#302 by dlesbre)

add hover provider (#300 by dlesbre)

add color to more keywords (#299 by dlesbre)

various improvements and consolidations (by Huỳnh Trần Khanh)

fixed leaking error message when only shelved goals remain (#268 by fakusb)

**@Zimmi48 (Théo Zimmermann)** posted in **Coq Platform 2022.09.1 release with Coq 8.16.1**

Dear Coq community,

On behalf of the Coq development team, the release manager of Coq 8.16, and the Coq Platform team, we are happy to announce the immediate availability of the Coq Platform 2022.09.1 release.

Release highlights:

- The latest version of Coq has been updated to 8.16.1, which fixes critical soundness bugs with previous versions, and brings other improvements (see the Coq release ...

**@palmskog (Karl Palmskog)** posted in **Volunteer co-maintainer needed for Docker-Coq**

The Coq Team and Coq-community are looking for a volunteer co-maintainer of the Docker-Coq project, which provides Docker container images of many versions of Coq as a service to Coq users.

Docker-Coq is an open source project on GitHub under the BSD-3-Clause license. It maintains definitions of a set of Docker images that provide a basic Coq environment for continuous integration and local use. ...

**@affeldt** posted in **MathComp 1.16.0 released**

We are proud to announce the immediate availability of the Mathematical Components library version 1.16.0.

The webpage, and documentation, are available at https://math-comp.github.io/.

This release is compatible with Coq 8.13, 8.14, 8.15, 8.16, and 8.17.

The contributors to this version are:

Cyril Cohen, Enrico Tassi, Erik Martin-Dorel, Georges Gonthier, Yoshihiro Ishiguro, Julien Puydt, Kazu...

**@ejgallego (Emilio Jesús Gallego Arias)** posted in **[ANN] coq-lsp release 0.1.5**

Dear all,

we are happy to announce the availability of coq-lsp 0.1.5, a Language Server and Visual Studio Code extension for the Coq Proof Assistant.

See the install instructions at the project’s page.

This release provides many bug fixes and quality of life improvements, in particular the goal panel has been much improved, and will now display information about bullets, shelved, and admitted

...

**@gares (Enrico Tassi)** posted in **[CUDW 2023] Coq Users and Developers Workshop - June 26 to 30 - Save the Date!**

Seventh Coq Users and Developers Workshop

`June 26th - June 30th, 2023 Sophia-Antipolis (Nice, France)`

The Coq Users and Developers Workshop is an event that brings together

the core developers of Coq and users interested in understanding,

improving or extending the system via its OCaml APIs or extension

languages such as Ltac2, MetaCoq or Elpi.

Its...

**@amahboubi (Assia Mahboubi)** posted in **PhD position at Inria / Nantes Université (France)**

We would like to invite applications for a 3 years fully-funded PhD

position within the Gallinette Inria research group at Nantes University (France).

The successful candidate will contribute to the Fresco ERC project,

aiming at designing fast and reliable symbolic computations. This

project involves topics in program verification as well as in

formalized mathematics.

The start date is ideal...

**@proux01 (Pierre Roux)** posted in **[ANN] Bignums release 9.0.0**

We just released Bignums 9.0.0 to remove the

`[_]%bigN`

,`[_]%bigZ`

and`[_]%bigQ`

notations that were causing too many conflicts (for

instance with`ListNotations`

or primitive arrays). We recommend using

`BigN.to_Z`

,`BigZ.to_Z`

and`BigQ.to_Q`

as backward compatible

replacements (until we find a less conflicting notation, suggestions

welcomed: Remove the [ _ ] notations by proux01 · Pull R...

**@pi8027 (Kazuhiko Sakaguchi)** posted in **Algebra Tactics 1.1.1 released**

Dear Mathematical Components users,

We are pleased to announce the release of Algebra Tactics 1.1.1.

In addition to the already provided ring and field tactics, this

release gives access to the lra, nra and psatz tactics from the

Micromega plugin shipped with Coq. For the moment, the new tactics are

considered experimental features and subject to change.

The new release is available in the O...

**@palmskog (Karl Palmskog)** posted in **Call for participation: ILDS Coq and Lean Autumn School 2023**

The LDS Coq and Lean Autumn School 2023 is an interactive theorem proving school that takes place September 18-20, 2023, in Bucharest, Romania.

Description

The ILDS Coq and Lean Autumn School 2023 aims to introduce potential students to the Coq and Lean proof assistants, as well as to theoretical underpinnings of interactive theorem proving. It is the second school on interactive theorem proving...

**@caverill (Charles Averill)** posted in **New Project - Implementing Haskell Curry's PhD Thesis on Combinatory Logic**

Hi! I’m an undergraduate student at the University of Texas at Dallas. I recently started using Coq, and more recently got interested in Combinatory Logic.

To feed my enthusiasm, I’ve started implementing definitions and proofs from the English translation of “Grundlagen der kombinatorischen Logik,” Haskell Curry’s 1930 PhD thesis in which the BCKW combinator calculus system is proposed. I’ve onl...

**@mattam82 (Matthieu Sozeau)** posted in **MetaCoq 1.2 release**

Dear Coq and MetaCoq users,

We are happy to announce that version 1.2 of the MetaCoq project has been released for Coq 8.16 and Coq 8.17, available both as source and through opam. It will also be part of the next Coq Platform. See the website for a detailed overview of the project, introductory material and related articles and presentations.

The main changes in this new version are (w.r.t. v1....

**@blanqui (Frédéric Blanqui)** posted in **3-year engineering position in Deducteam, Inria Paris-Saclay, France**

Deducteam is offering a 3-year engineering position to help develop, test and maintain tools for proof system interoperability (continuous integration, proof libraries management, searching tools, VSCode interface, etc.). Net taxable monthly salary between 2148 and 4412 euros depending on experience, including social security and 9 weeks holidays/year.

Interested people should send me their CV be...

**@ybertot (Yves Bertot)** posted in **2023 Coq workshop call for presentations**

We are pleased to invite you to submit presentation proposals for the

Coq Workshop 2023, which will be held in Białystok, Poland on July 31,

2023, as a satellite to the ITP conference.

https://coq-workshop.gitlab.io/2023/

The Coq Workshop 2023 is the 14th installment of the Coq Workshop

series. The workshop brings together users, contributors, and

developers of the Coq proof assistant.

The ...

**@affeldt** posted in **MathComp 1.17.0 released**

We are proud to announce the immediate availability of the Mathematical Components library version 1.17.0.

The webpage, and documentation, are available at https://math-comp.github.io/.

This release is compatible with Coq 8.15, 8.16, and 8.17.

The contributors to this version are:

Alex Gryzlov, Cyril Cohen, Jason Gross, Kazuhiko Sakaguchi, Kimaya Bedarkar,

Laurent Théry, Pierre Jouvelot, Pier...

**@proux01 (Pierre Roux)** posted in **MathComp 2.0.0 released**

We are proud to announce the immediate availability of the Mathematical Components library version 2.0.0.

:warning: Important :warning:

MathComp 2.x is not immediately compatible with version 1.17.0, i.e., porting your development to this new version may require more effort than usual. On the positive side, the entire hierarchy of structures and morphisms has been rewritten using the Hierarchy Builder tool (HB...

**@ybertot (Yves Bertot)** posted in **2nd Call for presentations: 2023 Coq workshop**

We are pleased to invite you to submit presentation proposals for the

Coq Workshop 2023, which will be held in Białystok, Poland on July 31,

2023, as a satellite to the ITP conference.

https://coq-workshop.gitlab.io/2023/

The Coq Workshop 2023 is the 14th installment of the Coq Workshop

series. The workshop brings together users, contributors, and

developers of the Coq proof assistant.

The ...

**@ybertot (Yves Bertot)** posted in **Deadline Extension: CfP 2023 Coq workshop, May 30th**

IMPORTANT: We are extending the deadline for submission to the

Coq workshop to May 30th, AoE (Anywhere on Earth).

We are pleased to invite you to submit presentation proposals for the

Coq Workshop 2023, which will be held in Białystok, Poland on July 31,

2023, as a satellite to the ITP conference.

https://coq-workshop.gitlab.io/2023/

The Coq Workshop 2023 is the 14th installment of the Coq W...

**@Zimmi48 (Théo Zimmermann)** posted in **Call for volunteer maintainers of CoqIDE**

The Coq core team and Coq-community are looking for volunteer maintainers of the CoqIDE project.

CoqIDE is an Integrated Development Environment (IDE) for Coq. CoqIDE is implemented using the OCaml programming language and the GTK3 widget toolkit for graphical user interfaces (GUIs). CoqIDE uses a legacy XML-based protocol to communicate with Coq and is licensed under the open source LGPL-2.1 lic...

**@fl233 (Frederic Loulergue)** posted in **Postdoctoral Position in Orleans, France: Collaborative Memory Models for Formal Verification**

A Post-Doctoral position is available as part of the funded ANR project CoMeMoV (https://comemov.github.io) between the LIFO (https://www.univ-orleans.fr/lifo/) (University of Orleans, France), CEA List (Home page) and Thales Research and Technology (Research and Technology | Thales Group).

Frama-C (https://www.frama-c.com/) is an extensible and collaborative open-source platform dedicated to sou...

**@patricoferris (Patrick Ferris)** posted in **Sherlocoq: Search released coq source-code**

Hello :wave:

First time here (I can usually be found doing things in OCaml). Recently, I’ve been getting my feet wet with writing Coq programs. Quite quickly I found myself missing the excellent Sherlocode we have in OCaml thanks to Arthur Wendling. Thankfully it’s quite OCaml agnostic, and I ported it to Coq and indexed the coq-released opam archive which you can find here: https://sherlocoq.sirref.o...

**@ejgallego (Emilio Jesús Gallego Arias)** posted in **[ANN] coq-lsp 0.1.7**

Hi folks,

it’s been a while, but we are happy to announce a new release of coq-lsp.

Install for Coq 8.17 and Visual Studio Code is as easy as:

$ opam install coq-lsp && code --install-extension ejgallego.coq-lspThe 0.1.7 release has been focused on refinement and bugfixes; we’d like to thank all the users and contributors for their feedback and work, and in particular Alex Sanchez-Stern who d...

**@Zimmi48 (Théo Zimmermann)** posted in **Coq Community Survey 2022 Results: Part IV and ITP paper announcement**

Coq Community Survey 2022 Results: Part IV and ITP paper announcement

TL;DR: This post completes a series of three previous posts (part I, part II, part III) with plots of answers to questions not yet analyzed in previous posts, and with the announcement of an article at ITP about the survey and the associated dataset.

The Coq Community Survey 2022 was organized by an ad hoc working group and con...

**@spitters (Bas Spitters)** posted in **CfP: Certified Programs and Proofs (CPP)**

Abstract Submission Deadline: 12 September 2023 at 23:59 AoE (UTC-12h)

Paper Submission Deadline: 19 September 2023 at 23:59 AoE (UTC-12h)

CPP welcomes submissions in research areas related to formal

certification of programs and proofs. The following is a

non-exhaustive list of topics of interest to CPP:

- certified or certifying programming, compilation, linking, OS

kernels, runtime syst...

**@rtetley (Romain Tetley)** posted in **[VsCoq 2] Call for beta-testers**

Hi everyone,

My name is Romain Tetley, I am the newly recruited engineer working full-time on VsCoq 2.

As some of you might have noticed, we have been rolling out pre-release versions of VsCoq 2 on the market place. Following this dynamic, we would like to make an official announcement as well as call for some beta-testers.

The first official release should be around the same time as coq 8.18 s...

**@stefanze (Stefan Zetzsche)** posted in **Workshop on Dafny at POPL 24**

**

** CALL FOR EXTENDED ABSTRACTS

**

** Dafny at POPL 2024

** 1st Workshop on the Dafny Programming and Verification Language

** 14th of January 2024, London, United Kingdom

**

** Submission Deadline:

** October 11, 2023

**

** https://popl24.sigplan.org/home/dafny-2024

** https://dafny24.hotcrp.com/

**OVERVIEW

Dafny is a verification-aware programming language that has native sup...

**@kstark (Kathrin Stark)** posted in **CoqPL 2024: Call for Presentations**

===================================================================

CoqPL 2024`10th International Workshop on Coq for Programming Languages -- January 20, 2024, co-located with POPL London, UK CALL FOR PRESENTATIONS https://popl24.sigplan.org/home/CoqPL-2024`

==========...

**@rtetley (Romain Tetley)** posted in **[VsCoq 2] Release**

Hi everyone,

The VsCoq team is proud to announce the first official release of VsCoq 2. This release aims at supporting Coq starting from version 8.18 and onwards.

Among the key features, VsCoq 2 introduces:A new continuous checking mode

[continuous-checking-short]

A customisable goal view

[goals_tabs]

A panel dedicated to launching queries

[query-panel]

Support for messages in the g...

**@Zimmi48 (Théo Zimmermann)** posted in **Coq Platform 2023.03.0 release with Coq 8.17.1**

Dear Coq community,

As the release manager of Coq 8.17, and on behalf of the Coq development team and the Coq Platform team, I am happy to announce the immediate availability of the Coq Platform 2023.03.0 release.

(This release is named after the month of March 2023, during which the initial Platform release was planned, but because of significant delays due to numerous issues when preparing ins...

**@rtetley (Romain Tetley)** posted in **[VsCoq 2] Patch Release 2.0.1**

Hi everyone,

As many of you have probably noticed, the 2.0.0 release broke a lot of your VsCoq set-ups.

What happenedSwitching to full release mode means that for most of you VsCoq automatically updated to 2.0.0. This is a problem because VsCoq 2 only supports Coq 8.18

On top of that the opam release of our language server did not go as planned (Package vscoq-language-server.2.0.0+coq8.18 by v...

**@rtetley (Romain Tetley)** posted in **[VsCoq Legacy] Release**

Hi everyone,

In order to help users who cannot yet migrate to Coq 8.18, we have decided to release VsCoq 1 as a separate extension: VsCoq Legacy.

It is now available on both the vscode marketplace and openvsx.

Romain, for the VsCoq team

**@stefanze (Stefan Zetzsche)** posted in **(2nd CfP) Dafny Workshop at POPL 24**

**

** Update: Program Committee

****

** CALL FOR EXTENDED ABSTRACTS

**

** Dafny at POPL 2024

** 1st Workshop on the Dafny Programming and Verification Language

** 14th of January 2024, London, United Kingdom

**

** Submission Deadline:

** October 11, 2023

**

** Dafny 2024 - POPL 2024

** https://dafny24.hotcrp.com/

**OVERVIEW

Dafny is a verification-aware programming language ...

**@adurier (Adrien Durier)** posted in **PhD Position in formal proofs @LMF/Université Paris-Saclay**

Bonjour à tous,

Je suis un utilisateur de Coq de longue date, mais j’utilise également d’autres outils de preuves formelle; aujourd’hui nous collaborons avec Burkhart Wolff sur Isabelle/HOL pour la validation de systèmes cyber-physiques, et je me permet de laisser ici une offre de thèse pour ce projet.

Si certains étudiants utilisateurs de Coq sont intéressés dans une thèse avec de la preuve for...

**@MonikaSeisenberger (Monika)** posted in **Permanent Post [L/SL] in Applied Formal Methods at Swansea University**

At Swansea we are looking for a new enthusiastic colleague in Applied Formal Methods. Maybe you know any researchers who would be interested to apply?

Closing Date: 09-10-2023Swansea University would be delighted to hear from interested parties who are pioneering new techniques and addressing new problems in applied formal methods, i.e., in applying mathematically grounded approaches such as ...

**@spitters (Bas Spitters)** posted in **PhD/postdoc vacancy on the verification of cryptographic protocols at Aarhus University**

We are looking for a strong PhD-candidate at Aarhus University (DK).

There may be possibilities for a postdoc position. Please contact me

for more information.

Project “Verified voting protocols and blockchains”.

A description of the project can be found below.

Deadline:1 November 2023.

https://phd.nat.au.dk/for-applicants/open-calls/november-2023/verified-voting-protocols-and-blockchains

T...

**@JoJoDeveloping (Johannes Hostert)** posted in **Iris 4.1 and std++ 1.9 released**

Hello everyone,

We are happy to announce the release of Iris 4.1 and std++ 1.9. Iris is a concurrent separation logic framework for Coq; for an overview of the numerous research projects employing Iris, see https://iris-project.org/. std++ is an extended “standard” library for Coq.

This Iris release mostly features quality-of-life improvements, such as smarter handling of ->/<- patterns by iDest...

**@rtetley (Romain Tetley)** posted in **[VsCoq 2] Release 2.0.2**

Hi everyone,

We are rolling out the latest minor release of VsCoq.

Among other things, this release:Makes various improvements to the goal view (such as auto-scrolling to the current goal)

Enables support for multiple byte UTF8 characters (solving known bugs)

Adds a status bar item indicating the current user set up (language server version, etc…)On behalf of the team, I would like to thank...

**@Lasse** posted in **Announcing Tactician version 1.0 beta2**

After almost three years of development, we are happy to announce Tactician 1.0 beta2. It is available for all

Coq versions between v8.12 and v8.18. Tactician is a proof

synthesis system that uses data from existing theorems in order to help users write new proofs. It can adapt

to, and learn from new developments on the fly. For details, see the website

and the list of publications.

Most of t...

**@affeldt** posted in **MathComp 2.1.0 released**

We are proud to announce the immediate availability of the Mathematical Components library version 2.1.0.

The webpage, and documentation, are available at https://math-comp.github.io/.

This release is compatible with Coq 8.16, 8.17, and 8.18.

The contributors to this version are:

Reynald Affeldt, Sophie Bernard, Alessandro Bruni, Fernando Chu,

Cyril Cohen, Josh Cohen, Hugo Deleye, Jason Gross...

**@proux01 (Pierre Roux)** posted in **MathComp 1.18.0 released**

We are proud to announce the immediate availability of the

Mathematical Components library version 1.18.0.

The webpage, and documentation, are available at https://math-comp.github.io/.

This release is compatible with Coq 8.16, 8.17 and 8.18

and includes changes from 2.1.0 that could be backported.

The contributors to this version are: Reynald Affeldt, Sophie

Bernard, Alessandro Bruni, Ferna...

**@emarzion (Evan Marzion)** posted in **Formally verified endgame tablebase generator**

Hello,

I would like to share a project I have been working on, a formally verified endgame tablebase generator, written in Coq.

Here is the project code. I also wrote a blog post explaining the project and some of the design choices I made, which you can read here. Finally, you can play around with some of the results I generated for a sample game here.

**@palmskog (Karl Palmskog)** posted in **Call for volunteer maintainers of the Coq Library of Complexity Theory**

Coq-community is looking for looking for volunteer maintainers of the Coq Library of Complexity Theory project.

As per the name, the library contains definitions and results related to computational complexity formalized in Coq, including NP-hardness, the Cook-Levin Theorem, NP-completeness results, and resource analysis of call-by-value lambda-calculus and Turing machines. Results from the libra...

**@ejgallego (Emilio Jesús Gallego Arias)** posted in **[ANN] coq-lsp 0.1.8**

Dear all,

the 0.1.8 release of coq-lsp is out.

This release brings important fixes and a few performance improvements; in particular editing inside opaque proofs should behave much better w.r.t. incremental engine; formatting inside the error and

message panels has been fixed, as well as display for light mode.

On the protocol side, the LSP textDocument/selectionRange method is now supported, ...

**@dankoi** posted in **Internships at CNES, the French space agency**

A number of internship available for French students at CNES, the French space agency, including a research internship in proof theory here: Emploi CNES - Arbres de défaillances et formes normales exp-log Stage, 4-6 mois

**@rtetley (Romain Tetley)** posted in **[VsCoq 2] Release 2.0.3**

Hi everyone,

We are rolling out the latest minor release of VsCoq.

We have mainly been working on stability and bug fixes, in this release you’ll find :Some improvements to performance on large files

Fixing document state invalidation bugs

Goal view improvementsOn behalf of the team we would like to thank the community for helping to improve VsCoq.

Special thanks to dlesbre and tomtomjhj f...

**@Yannick_Forster** posted in **MetaCoq tutorial at POPL on Sunday, January 14th**

Dear all,

as part of POPL's TutorialFest, we will run a tutorial on MetaCoq.The tutorial will happen on Sunday, January 14th, i.e. on the day before CPP.

In this tutorial, we will present the MetaCoq library of Coq and the meta-programming features it provides. MetaCoq allows users to write meta-programs on Coq terms and to specify and verify those programs w.r.t. the metatheory of Coq, wh...

**@alexjbest (Alex J. Best)** posted in **Interactions Between Proof Assistants and Mathematical Software at ICMS 2024 (call for abstracts)**

We are happy to announce that we will run a session on Interactions Between Proof Assistants and Mathematical Software at the biannual International Conference on Mathematical Software in Durham, UK 22-25 July 2024.

As part of this we are calling for abstracts for talks to be presented at the session. Abstracts should be around 200 words. The short abstract deadline is the 24th February 2024, bu...

**@palmskog (Karl Palmskog)** posted in **VLSM 1.3 release**

The CBC Team at Runtime Verification, Inc. is happy to announce release 1.3 of VLSM, a Coq framework for modeling and verifying distributed systems executing in the presence of faults. The framework is available as the package coq-vlsm in Coq’s package index and is compatible with Coq 8.16, 8.17 and 8.18.

The framework builds on the theory Validating Labelled State Transition and Message Producti...

**@faenuccio (Filippo A. E. Nuccio)** posted in **Master Program on Formalised Math**

A 2nd year master program on higher algebra and formalised mathematics will be proposed next year (2024/25) in Lyon (France) as part of the joint Master Program of Lyon University, Saint-Étienne University and École Normale Supérieure de Lyon: the details are available here.

Two courses (one per term) will be devoted to formalising mathematics in Lean and one course in the second term will be dev...

**@florath (Andreas Florath)** posted in **Experiment: Coq Code Interpreter in ChatGPT**

Hello!

I created a Custom GPT that is able to interact with a Coq runtime environment. This is a new way to interact with Coq. It is very similar to the built-in python code interpreter: ChatGPT is able to check the correctness first and fix problems before presenting the result to the user.

It is possible to ask for help like:

Help me understand this Coq code [COQ]Check S (S 0).[\COQ]But als...

**@Lasse** posted in **Announcing Graph2Tac, a prover based on Tactician's new API**

We are pleased to announce Tactician’s API, a new AI interface for theorem

proving, building on Tactician. This includes a new graph-based dataset of

over 520k definitions (of which 260k are theorems) in 120 Coq packages, one of

the largest datasets for AI interactive theorem proving. We also present a new

state-of-the-art neural theorem proving solver Graph2Tac, designed for proving

theorems...

**@Laurent_Thery** posted in **MathComp 2.2.0 and 1.19.0 released**

We are proud to announce the immediate availability of the Mathematical Components library versions 2.2.0 and 1.19.0.

The webpage, and documentation, are available at https://math-comp.github.io/.

This release is compatible with Coq 8.16 to 8.19

The main change is compatibility with Coq 8.19.

The contributors to this version are: Reynald Affeldt, Cyril Cohen, Pierre Pomeret-Coquot, Pierre Roux...

**@caverill (Charles Averill)** posted in **VOLPIC: A verification pipeline for Pascal**

Today I released the source for VOLPIC, a verification pipeline I’ve been developing for the Pascal programming language: https://github.com/CharlesAverill/volplic

[logo_black]

VOLPIC parses log files from the Free Pascal Compiler to obtain a structured, compiler-checked representation of a program, converts that structure to an AST representing Gallina code, and generates a Coq file containing...

**@rtetley (Romain Tetley)** posted in **[VsCoq 2] Release 2.1.0**

Hi everyone,

We are pleased to announced v2.1.0 of VsCoq. This release mainly introduces coq 8.19 compatibility among other minor fixes.

Thanks to the Coq Core team for their various adaptations to the new Coq API.

Thanks to LittleJianCH and afdw for their contributions.

Romain for the VsCoq team

**@ybertot (Yves Bertot)** posted in **ITP 2024 : Second call for papers**

The international conference on Interactive Theorem Proving (ITP 2024)

will take place on September 9-14, 2024 in Tbilisi, Georgia. It is

planned as a hybrid meeting. It will mostly be a face-to-face (physical)

meeting but facilities will be provided for remote presentation and

remote attendance.

The ITP conference series is concerned with all aspects of interactive

theorem proving, rangi...

**@rtetley (Romain Tetley)** posted in **[VsCoq 2] Release 2.1.2**

Hi everyone,

We are pleased to announce the next minor release of VsCoq.

This release introduces a number of fixes and improves the stability of VsCoq.

We have also added some minor features such as enabling navigation commands in continuous mode.

We’re planning for another release in the coming month, stay tuned for some more improvements !

Romain, for the VsCoq team

**@mercicle (John Mercer)** posted in **[RFC] EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages**

EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages

EvoGPT on arXiv

Abstract

Formal mathematics is the discipline of translating mathematics into a programming language in which any statement can be unequivocally checked by a computer. Mathematicians and computer scientists have spent decades of painstaking formalization efforts developing languages such as Coq, HOL, ...

Last updated: Mar 02 2024 at 16:01 UTC