Stream: Announcements

Topic: New announcements on Discourse


view this post on Zulip Discourse Bot (Jun 19 2020 at 10:25):

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...

view this post on Zulip Discourse Bot (Jun 19 2020 at 10:25):

@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...

view this post on Zulip Discourse Bot (Jun 19 2020 at 10:25):

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...

view this post on Zulip Discourse Bot (Jun 19 2020 at 10:26):

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 ...

view this post on Zulip Théo Zimmermann (Jun 19 2020 at 10:28):

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).

view this post on Zulip Discourse Bot (Jun 19 2020 at 14:40):

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

view this post on Zulip Discourse Bot (Jun 19 2020 at 14:52):

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...

view this post on Zulip Discourse Bot (Jun 20 2020 at 12:45):

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!

view this post on Zulip Discourse Bot (Jun 26 2020 at 15:40):

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...

view this post on Zulip Discourse Bot (Jul 02 2020 at 12:53):

@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...

view this post on Zulip Discourse Bot (Jul 03 2020 at 08:25):

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...

view this post on Zulip Discourse Bot (Jul 03 2020 at 08:42):

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...

view this post on Zulip Discourse Bot (Jul 05 2020 at 15:15):

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...

view this post on Zulip Discourse Bot (Jul 15 2020 at 15:58):

@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...

view this post on Zulip Discourse Bot (Jul 18 2020 at 23:10):

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

view this post on Zulip Discourse Bot (Jul 27 2020 at 18:05):

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:

view this post on Zulip Discourse Bot (Aug 19 2020 at 07:29):

@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...

view this post on Zulip Discourse Bot (Sep 04 2020 at 11:57):

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...

view this post on Zulip Discourse Bot (Sep 06 2020 at 09:07):

@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

====...

view this post on Zulip Discourse Bot (Sep 08 2020 at 14:10):

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...

view this post on Zulip Discourse Bot (Sep 16 2020 at 14:17):

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,...

view this post on Zulip Discourse Bot (Sep 24 2020 at 12:00):

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

(Apologies for possible cross-posting.)
The Thirteenth NASA Formal Methods Symposium

https://shemesh.larc.nasa.gov/nfm2021/
24-28 May 2021
Norfolk, VA, USA

The 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...

view this post on Zulip Discourse Bot (Oct 08 2020 at 02:25):

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...

view this post on Zulip Discourse Bot (Oct 09 2020 at 10:20):

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 at

Crowdsourcing a CU...

view this post on Zulip Discourse Bot (Oct 14 2020 at 21:01):

@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...

view this post on Zulip Discourse Bot (Nov 07 2020 at 03:23):

@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...

view this post on Zulip Discourse Bot (Nov 15 2020 at 20:07):

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...

view this post on Zulip Discourse Bot (Nov 16 2020 at 14:12):

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...

view this post on Zulip Discourse Bot (Nov 26 2020 at 11:03):

@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...

view this post on Zulip Discourse Bot (Dec 04 2020 at 16:59):

@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 ...

view this post on Zulip Discourse Bot (Dec 07 2020 at 01:00):

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 ...

view this post on Zulip Discourse Bot (Dec 09 2020 at 09:57):

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:

view this post on Zulip Discourse Bot (Dec 11 2020 at 09:06):

@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...

view this post on Zulip Discourse Bot (Dec 11 2020 at 21:40):

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

view this post on Zulip Discourse Bot (Dec 24 2020 at 11:08):

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 ...

view this post on Zulip Discourse Bot (Jan 12 2021 at 11:51):

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:

view this post on Zulip Discourse Bot (Jan 13 2021 at 17:08):

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...

view this post on Zulip Discourse Bot (Feb 17 2021 at 17:07):

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...

view this post on Zulip Discourse Bot (Feb 22 2021 at 07:33):

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 ...

view this post on Zulip Discourse Bot (Feb 23 2021 at 18:38):

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:

view this post on Zulip Discourse Bot (Feb 26 2021 at 16:54):

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...

view this post on Zulip Discourse Bot (Mar 04 2021 at 15:12):

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...

view this post on Zulip Discourse Bot (Mar 15 2021 at 10:31):

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...

view this post on Zulip Discourse Bot (Mar 17 2021 at 11:04):

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...

view this post on Zulip Discourse Bot (Mar 27 2021 at 09:35):

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 ...

view this post on Zulip Discourse Bot (Apr 02 2021 at 08:43):

@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!

view this post on Zulip Discourse Bot (Apr 08 2021 at 12:43):

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...

view this post on Zulip Discourse Bot (Apr 12 2021 at 14:29):

@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...

view this post on Zulip Discourse Bot (Apr 13 2021 at 10:03):

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...

view this post on Zulip Discourse Bot (Apr 14 2021 at 12:56):

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...

view this post on Zulip Discourse Bot (May 06 2021 at 06:52):

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...

view this post on Zulip Discourse Bot (Jun 07 2021 at 13:17):

@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...

view this post on Zulip Discourse Bot (Jun 18 2021 at 19:25):

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/
------------...

view this post on Zulip Discourse Bot (Jun 21 2021 at 15:07):

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,...

view this post on Zulip Discourse Bot (Jul 23 2021 at 16:15):

@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...

view this post on Zulip Discourse Bot (Sep 06 2021 at 15:40):

@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...

view this post on Zulip Discourse Bot (Sep 08 2021 at 15:14):

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...

view this post on Zulip Discourse Bot (Sep 15 2021 at 15:31):

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, 2022

Overview
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...

view this post on Zulip Discourse Bot (Sep 23 2021 at 17:51):

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 ...

view this post on Zulip Discourse Bot (Oct 28 2021 at 14:13):

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...

view this post on Zulip Discourse Bot (Nov 01 2021 at 00:24):

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, ...

view this post on Zulip Discourse Bot (Nov 08 2021 at 13:07):

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...

view this post on Zulip Discourse Bot (Nov 08 2021 at 16:59):

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...

view this post on Zulip Discourse Bot (Nov 08 2021 at 19:45):

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]

view this post on Zulip Discourse Bot (Jan 17 2022 at 17:04):

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...

view this post on Zulip Discourse Bot (Jan 19 2022 at 12:19):

@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...

view this post on Zulip Discourse Bot (Jan 24 2022 at 15:42):

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.
...

view this post on Zulip Discourse Bot (Jan 27 2022 at 19:17):

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:

view this post on Zulip Discourse Bot (Jan 29 2022 at 12:04):

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...

view this post on Zulip Discourse Bot (Feb 10 2022 at 10:23):

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...

view this post on Zulip Discourse Bot (Feb 16 2022 at 19:06):

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 ...

view this post on Zulip Discourse Bot (Mar 10 2022 at 16:09):

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...

view this post on Zulip Discourse Bot (Mar 12 2022 at 23:40):

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...

view this post on Zulip Discourse Bot (Mar 16 2022 at 13:57):

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).

view this post on Zulip Discourse Bot (Mar 16 2022 at 17:41):

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 ...

view this post on Zulip Discourse Bot (Mar 21 2022 at 17:56):

É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...

view this post on Zulip Discourse Bot (Mar 29 2022 at 02:01):

É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...

view this post on Zulip Discourse Bot (Mar 29 2022 at 09:50):

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 ...

view this post on Zulip Discourse Bot (Mar 29 2022 at 12:24):

@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...

view this post on Zulip Discourse Bot (Mar 31 2022 at 07:51):

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...

view this post on Zulip Discourse Bot (Apr 10 2022 at 07:12):

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, 2022

Application deadline
15 April 2022

Overview
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 ...

view this post on Zulip Discourse Bot (Apr 21 2022 at 13:28):

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:

view this post on Zulip Discourse Bot (Apr 30 2022 at 12:30):

@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...

view this post on Zulip Discourse Bot (May 04 2022 at 12:00):

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...

view this post on Zulip Discourse Bot (May 11 2022 at 16:45):

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!

view this post on Zulip Discourse Bot (Jun 20 2022 at 19:55):

@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...

view this post on Zulip Discourse Bot (Jun 23 2022 at 09:28):

@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 project ADAM: 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...

view this post on Zulip Discourse Bot (Jun 27 2022 at 08:30):

@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:

view this post on Zulip Discourse Bot (Jun 30 2022 at 09:37):

@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 ...

view this post on Zulip Discourse Bot (Jul 05 2022 at 13:54):

@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...

view this post on Zulip Discourse Bot (Jul 07 2022 at 08:50):

@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 ...

view this post on Zulip Discourse Bot (Jul 11 2022 at 13:06):

@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...

view this post on Zulip Discourse Bot (Jul 12 2022 at 12:53):

@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...

view this post on Zulip Discourse Bot (Jul 13 2022 at 12:54):

@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 ...

view this post on Zulip Discourse Bot (Aug 03 2022 at 14:40):

@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
...

view this post on Zulip Discourse Bot (Aug 16 2022 at 14:29):

@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
mathcomp

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

view this post on Zulip Discourse Bot (Aug 20 2022 at 11:58):

@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...

view this post on Zulip Discourse Bot (Aug 30 2022 at 07:52):

@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...

view this post on Zulip Discourse Bot (Aug 31 2022 at 11:38):

@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...

view this post on Zulip Discourse Bot (Sep 02 2022 at 20:51):

@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...

view this post on Zulip Discourse Bot (Sep 27 2022 at 18:50):

@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...

view this post on Zulip Discourse Bot (Oct 05 2022 at 07:50):

@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...

view this post on Zulip Discourse Bot (Oct 11 2022 at 13:52):

@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:

view this post on Zulip Discourse Bot (Oct 12 2022 at 12:36):

@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...

view this post on Zulip Discourse Bot (Oct 12 2022 at 14:16):

@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...

view this post on Zulip Discourse Bot (Oct 14 2022 at 22:29):

@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...

view this post on Zulip Discourse Bot (Oct 27 2022 at 16:44):

@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...

view this post on Zulip Discourse Bot (Nov 14 2022 at 13:27):

@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...

view this post on Zulip Discourse Bot (Nov 18 2022 at 15:01):

@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...

view this post on Zulip Discourse Bot (Dec 19 2022 at 14:38):

@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

view this post on Zulip Discourse Bot (Dec 24 2022 at 11:44):

@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

view this post on Zulip Discourse Bot (Jan 08 2023 at 18:40):

@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...

view this post on Zulip Discourse Bot (Jan 11 2023 at 06:14):

@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...

view this post on Zulip Discourse Bot (Jan 11 2023 at 15:26):

@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)

view this post on Zulip Discourse Bot (Jan 17 2023 at 12:42):

@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:

view this post on Zulip Discourse Bot (Jan 17 2023 at 16:07):

@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. ...

view this post on Zulip Discourse Bot (Feb 02 2023 at 07:08):

@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...


Last updated: Feb 06 2023 at 05:03 UTC