Discourse Bot (Jun 19 2020 at 10:25): 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...
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...
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...
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 ...
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).
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
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...
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!
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...
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...
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...
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...
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...
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...
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
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:
- 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...
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...
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...
Discourse Bot (Sep 06 2020 at 09:07):@amintimany posted in CoqPL 2021: Call for Presentations
===================================================================
CoqPL 20217th 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====...
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...
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,...
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 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...
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...
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 atCrowdsourcing a CU...
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...
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...
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...
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...
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...
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 ...
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 ...
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:
- 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...
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...
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
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 ...
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:
Introduction of primitive persistent arrays in the core language,
implemented using imperative persistent arrays.Introduction of definition...
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...
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...
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 ...
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:
- Fix arities of VM opcodes for some floating-point operations that
could cause memory corruption.
Best,
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...
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...
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...
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...
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 ...
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!
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...
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...
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...
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...
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...
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...
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/
------------...
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,...
Discourse Bot (Jul 23 2021 at 16:15):@amintimany posted in CoqPL 2022: Call for Presentations
===================================================================
CoqPL 20228th 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...
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-2022WITS 2022 is the first Workshop on the Implementation of Type
Systems. The workshop will be held on January 22, 2022, in
Phi...
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...
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, 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...
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 ...
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...
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, ...
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...
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...
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]
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...
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...
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.
...
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:
- An important newly added package, coq-hammer, provides the hammer
tactic, which uses external ATPs (Automated Theorem Provers) to
automatically cr...
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...
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...
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 ...
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...
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...
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).
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 ...
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...
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...
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 ...
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...
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...
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, 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 ...
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:
- 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...
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...
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...
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!
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...
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...
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:
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...
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 ...
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...
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 onCERTIFIED AND SYMBOLIC-NUMERIC COMPUTATIONwill 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 ...
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...
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...
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 ...
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
...
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
mathcompA list of Coq Kata is available through the Kata search page. The original request for Coq 8.15 support can be found...
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...
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...
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...
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...
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...
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...
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:
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...
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...
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...
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...
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...
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...
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...
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
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
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...
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...
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)
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:
- 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 ...
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. ...
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...
Discourse Bot (Feb 15 2023 at 21:27):@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
...
Discourse Bot (Mar 01 2023 at 13:09):@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...
Discourse Bot (Mar 04 2023 at 10:11):@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...
Discourse Bot (Mar 20 2023 at 09:20):@proux01 (Pierre Roux) posted in [ANN] Bignums release 9.0.0
We just released Bignums 9.0.0 to remove the
[_]%bigN,[_]%bigZ
and[_]%bigQnotations that were causing too many conflicts (for
instance withListNotationsor primitive arrays). We recommend using
BigN.to_Z,BigZ.to_ZandBigQ.to_Qas backward compatible
replacements (until we find a less conflicting notation, suggestions
welcomed: Remove the [ _ ] notations by proux01 · Pull R...
Discourse Bot (Apr 13 2023 at 13:12):@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...
Discourse Bot (Apr 13 2023 at 21:13):@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...
Discourse Bot (Apr 21 2023 at 05:16):@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...
Discourse Bot (Apr 22 2023 at 12:42):@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....
Discourse Bot (Apr 22 2023 at 14:34):@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...
Discourse Bot (Apr 25 2023 at 07:03):@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 ...
Discourse Bot (May 10 2023 at 06:51):@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...
Discourse Bot (May 15 2023 at 06:35):@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...
Discourse Bot (May 16 2023 at 08:30):@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 ...
Discourse Bot (May 26 2023 at 16:17):@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...
Discourse Bot (Jun 02 2023 at 12:34):@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...
Discourse Bot (Jun 10 2023 at 10:38):@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...
Discourse Bot (Jun 18 2023 at 13:50):@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...
Discourse Bot (Jul 11 2023 at 10:57):@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...
Discourse Bot (Jul 28 2023 at 09:28):@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...
Discourse Bot (Aug 14 2023 at 18:34):@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...
Discourse Bot (Aug 24 2023 at 12:23):@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...
Discourse Bot (Aug 31 2023 at 11:11):@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...
Discourse Bot (Sep 14 2023 at 17:22):@kstark (Kathrin Stark) posted in CoqPL 2024: Call for Presentations
===================================================================
CoqPL 202410th 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==========...
Discourse Bot (Sep 15 2023 at 15:57):@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...
Discourse Bot (Sep 18 2023 at 15:38):@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...
Discourse Bot (Sep 20 2023 at 08:05):@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...
Discourse Bot (Sep 20 2023 at 15:34):@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
Discourse Bot (Sep 27 2023 at 14:34):@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 ...
Discourse Bot (Sep 28 2023 at 12:48):@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...
Discourse Bot (Sep 28 2023 at 15:22):@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 ...
Discourse Bot (Oct 11 2023 at 10:58):@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...
Discourse Bot (Oct 12 2023 at 19:32):@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...
Discourse Bot (Oct 17 2023 at 05:58):@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...
Discourse Bot (Oct 23 2023 at 03:37):@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...
Discourse Bot (Oct 25 2023 at 13:25):@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...
Discourse Bot (Nov 01 2023 at 10:53):@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...
Discourse Bot (Nov 05 2023 at 18:22):@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.
Discourse Bot (Nov 08 2023 at 21:41):@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...
Discourse Bot (Nov 14 2023 at 16:24):@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, ...
Discourse Bot (Nov 27 2023 at 17:39):@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
Discourse Bot (Dec 05 2023 at 16:38):@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...
Discourse Bot (Dec 12 2023 at 16:17):@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...
Discourse Bot (Dec 18 2023 at 01:11):@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...
Discourse Bot (Dec 22 2023 at 21:13):@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...
Discourse Bot (Jan 08 2024 at 14:53):@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...
Discourse Bot (Jan 09 2024 at 06:59):@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...
Discourse Bot (Jan 12 2024 at 15:16):@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...
Discourse Bot (Jan 18 2024 at 10:13):@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...
Discourse Bot (Feb 08 2024 at 04:19):@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...
Discourse Bot (Feb 13 2024 at 10:39):@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
Discourse Bot (Feb 16 2024 at 07:55):@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...
Discourse Bot (Feb 21 2024 at 14:01):@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
Discourse Bot (Feb 28 2024 at 14:49):@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, ...
Discourse Bot (Mar 04 2024 at 12:59):@SkySkimmer (Gaëtan Gilbert) posted in Coq 8.19.1
The tag for 8.19.1 has been set to commit 8152d125abb0fb7e8cbecf4bd6cd51d8d3e70d78.
Coq 8.19.1 fixes a number of bugs, most notably:
- incorrect abstraction of sort variables for opaque constants leading to an inconsistency (Missing abstraction of const_relevance for opaques (Anomaly "File "kernel/cClosure.ml", line 138, characters 6-12: Assertion failed.") · Issue #18594 · coq/coq · GitHub)
- ...
Discourse Bot (Mar 19 2024 at 10:55):@mattam82 (Matthieu Sozeau) posted in MetaCoq 1.3.1 release
We are happy to announce release 1.3.1 of the MetaCoq project for Coq 8.17, 8.18 and 8.19, available both as source and through opam. This release will be part of the upcoming Coq Platform release including Coq 8.19. See the website for a detailed overview of the project, introductory material and related articles and presentations.
The main changes in this new version w.r.t. v1.2.1 are:A full...
Discourse Bot (Mar 22 2024 at 14:19):@rob.y.lewis (Robert Y. Lewis) posted in Annals of Formalized Mathematics
Filippo Nuccio and I are very excited to announce the launch of the Annals of Formalized Mathematics!
The AFM is a MathOA-supported diamond open access overlay journal. It publishes original articles about formalized mathematics and mathematical applications of proof assistants, spanning many proof assistant ecosytems. Papers should be written for an audience of mathematicians and should not focu...
Discourse Bot (Mar 26 2024 at 06:12):@bmontagu (Benoît Montagu) posted in Volunteers for ICFP 2024 Artifact Evaluation Committee (AEC)
Dear all,
We are looking for motivated people to be members of the ICFP 2024
Artifact Evaluation Committee (AEC). Students, researchers and people
from the industry or the free software community are all welcome. The
artifact evaluation process aims to improve the quality and
reproducibility of research artifacts for ICFP papers. In case you
want to nominate someone else (students, colleague...
Discourse Bot (Apr 11 2024 at 18:39):@caverill (Charles Averill) posted in Yet Another Tactics Index for Beginners
https://charlesaverill.github.io/ctpe/
I’ve been using Coq for a little longer than a year now. One of the things that left me very apprehensive about learning more about the system was the (in my opinion) poor availability of simple explanations of tactics. There are a few intro to tactics lists, but they focus a lot on the tactics that I was able to figure out on my own. So I decided to write y...
Discourse Bot (Apr 12 2024 at 13:23):@RalfJ posted in Iris 4.2 and std++ 1.10
Hi everyone,
We are happy to announce the release of Iris 4.2 and std++ 1.10. 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 of this new Iris version are:We have new laws to “undiscard” discarded fractions, allowing one to u...
Discourse Bot (Apr 12 2024 at 14:24):@ppedrot (Pierre Marie Pédrot) posted in [CUDW 2024] Coq User And Developers Workshop 2024 — July 1st - July 5th — Save the date!
Eigth Coq Users and Developers Workshop
July 1st - July 5th, 2024 Nantes Université (Nantes, 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 eigth editio...
Discourse Bot (Apr 22 2024 at 11:34):@CohenCyril (Cyril Cohen) posted in First Mathcomp sharing day
Dear Rocq/Coq and Mathematical components library users, we are pleased to announce our first “Mathcomp sharing day”. On April 24th 2024, From 10am to 5pm Paris time, mathcomp users, from enthusiasts to experts, are welcome to casually meetup online and engage in various activity among which: contributing to mathcomp (fixing bugs, solving issues, adding features, integrating external developments ...
Discourse Bot (Apr 29 2024 at 07:02):@TheoWinterhalter (Théo Winterhalter) posted in Coq Workshop 2024 call for presentations
We are pleased to invite you to submit presentation proposals for the Coq Workshop 2024, which will be held in Tbilisi, Georgia on 13 September 2024, as a satellite to the ITP conference.
The Coq Workshop 2024 is the 15th instalment of the Coq Workshop series. The workshop brings together users, contributors, and developers of the Coq proof assistant.
The Coq Workshop focuses on strengthening th...
Discourse Bot (Apr 30 2024 at 07:41):@sacerdot (Claudio Sacerdoti Coen) posted in Deadline Extension: Logical Frameworks and Meta Languages: Theory and Practice (LFMTP24)
Notice: due to multiple requests, the deadlines for LFMTP24 have been
extended as follow:abstract submission: May 6
paper submission: May 13Here is the updated CfP.
====================================================================
Logical Frameworks and Meta Languages: Theory and Practice
(LFMTP24)
https://lfmtp.github.io/lfmtp-page/workshops/2024/============================...
Discourse Bot (May 05 2024 at 21:48):@Yutaka posted in [WAIT2024] Call for Contributions: Fifth International Workshop on Automated (Co)inductive Theorem Proving
Call for Contributions: Fifth International Workshop on Automated (Co)inductive Theorem Proving
Dear Coq users,
(Please accept our apologies if you receive this call through multiple channels. We aim to ensure that all potentially interested parties are informed, but sometimes this leads to overlaps.)
We are delighted to announce the Fifth International Workshop on Automated (Co)inductive Theore...
Discourse Bot (May 22 2024 at 09:50):@CohenCyril (Cyril Cohen) posted in Second Mathcomp sharing day
Dear Rocq/Coq and Mathematical components library users, we are pleased to announce our first “Mathcomp sharing day”. On May 29th 2024, From 9am to 5pm Paris time, mathcomp users, from enthusiasts to experts, are welcome to casually meetup online and engage in various activity from contributing to mathcomp (fixing bugs, solving issues, adding features, integrating external developments to mathcomp...
Discourse Bot (May 31 2024 at 14:51):@ejgallego (Emilio Jesús Gallego Arias) posted in [ANN] coq-lsp 0.1.9
Dear all,
We are happy to announce the 0.1.9 release of coq-lsp.
This release brings many new features and fixes, in particular:New on-demand checking mode: coq-lsp can now check files on
demand, either by following the goals requested, or by following the
current viewport of your editor. Combined with the new keybinding
M-n/M-p for moving between Coq sentences, this provides a mode
simi...
Discourse Bot (Jun 10 2024 at 11:29):@SkySkimmer (Gaëtan Gilbert) posted in Coq 8.19.2
The tag for 8.19.2 has been set to commit d739f8d6f60d623fe20933a8506e53f3d6391eaa.
Coq 8.19.2 fixes a number of bugs.
Coq 8.19.2 is compatible with memprof-limits interruption methods. This
means that Coq will be recompiled when the library is installed /
removed from an OPAM switch.
See the changelog Recent changes — Coq 8.19.1 documentation for details.
Discourse Bot (Jun 13 2024 at 13:11):@CohenCyril (Cyril Cohen) posted in [Postdoc position] Machine Learning for translation between formal mathematics libraries
Dear Coq users,
I would like to attract your attention to an open position at ENS Lyon on the translation between formal mathematics libraries using machine learning techniques.Best wishes.
Discourse Bot (Jun 19 2024 at 16:06):@proux01 (Pierre Roux) posted in Call for volunteer maintainers of math-classes and CORN
Coq-community is looking for volunteer additional maintainers of the math-classes and CORN projects.
The libraries contain definitions and results related to real numbers formalized in Coq.
The project has been largely maintained for years by coq-community and coq developers (as part of Coq CI) and currently supports Coq 8.19 and Coq master. An initial task for a new maintainer would be to keep...
Discourse Bot (Jun 25 2024 at 08:45):@rtetley (Romain Tetley) posted in [VsCoq2] Release 2.1.3
Hi everyone,
We are pleased to announce the next minor release of VsCoq.
This release introduces a number of fixes but most notably:A new highlight system with better visualisations in manual mode and improved performance
[vscoq_highlights]
Note that we now discriminate between “Prepared”, “Processing” and “Processed”, which is helpful when computations take a long time
[vscoq_highlights_de...
Discourse Bot (Jul 01 2024 at 10:15):@proux01 (Pierre Roux) posted in Coq 8.20+rc1
The release candidate for Coq 8.20 is now available. Library authors
can safely start preparing compatible releases. For continuous
integration purposes, the release candidate is available as a Docker
image [1] as well as in nixpkgs, in particular through the
coq-nix-toolbox [2]. The final 8.20.0 release is planned for early
September.
[1] https://hub.docker.com/r/coqorg/coq/tags?page=&page_...
Discourse Bot (Jul 02 2024 at 08:41):@andreas.huelsing (Andreas Hülsing) posted in [Assistant Professor, TU Eindhoven, NL] Formal Verification of Cryptographic Implementations
Hi all, I have an opening for an assistant professor on machine-checking / formally verifying cryptographic implementations. Although experience with cryptography is a big plus, I would also consider candidates with experience in verifying functional correctness for other applications (if you are willing to look at cryptography).
The opening is here:If you have questions, feel free to reach ou...
Discourse Bot (Jul 02 2024 at 14:22):@mkerjean (Marie Kerjean) posted in CFP - JFLA 2025 - Journées Francophones des Langages Applicatifs
This message is intentionally written in French. It is a call for
papers for the “Francophone Days on Functional Languages” to be held
at the end of January 2025 in the Loire Valley. Papers can be written in
English, but the presentations themselves are expected to be given in
French.
Merci de faire circuler : premier appel à communications
JFLA 2025 : Journées Francophones des Langages Appl...
Discourse Bot (Jul 08 2024 at 13:28):@rtetley (Romain Tetley) posted in [VsCoq] Release 2.1.4
Hey everyone,
We are rolling out another minor release of VsCoq.
This is just to get a few blocking display and server bugs fixed quickly.
Note that this version is compatible with vscoq-language-server v2.1.3, so it will still work even though we are waiting for the release on opam of v2.1.4.
Thanks to @FissoreD, @Durbatuluk1701 for their contributions as well as the Coq Core team for their a...
Discourse Bot (Jul 13 2024 at 06:52):@KatyaKom (Ekaterina) posted in PhD in Coq Formalisation of Differentiable Logics
Hello, we are looking for a PhD student to work on Coq formalisation of Differentiable Logics, the full details are below.
Vacancy: PhD in Computer Science
Title: Formal Verification of AI Interfaces
Advisors: Ekaterina Komendantskaya (Southampton University, UK), Alessandro Bruni (IT University of Copenhagen, Denmark), Reynald Affeldt (AIST, Japan)
Start Date: As soon as the right candidate i...
Discourse Bot (Jul 18 2024 at 12:39):@thomas-lamiaux (Thomas Lamiaux) posted in Coq Platform Docs: a documentation project for Coq and its Platform
Dear Coq users and developpers,
We would like to shed some light on our new project “Coq Platform Docs”.
Our goal is to provide an online compilation of short, practical and interactive
tutorials and how-to guides about Coq and the Coq Platform. We wish this content
to be part of the upcoming Rocq website. A detailed description of the project can
be found in our Coq Enhancement Proposal (CEP...
Discourse Bot (Jul 22 2024 at 13:55):@erikmd (Erik Martin Dorel) posted in ANN: docker-coq: Bump to Debian 12 (& opam 2.2.0)
TL;DR: if you use docker-coq images and install Debian packages in your CI script (manually or via opam depext), then you might be impacted by the upgrade planned on next Monday 2024-07-27.
Similarly to last time, we would like to announce some upcoming version bump for the base image of docker-coq → using the last stable release of Debian (bookworm) on next Monday, 2024-07-27. The upgrade will ...
Discourse Bot (Jul 23 2024 at 14:54):@mattam82 (Matthieu Sozeau) posted in Verified Extraction for Coq 8.19
We are happy to announce version 0.9.2 of the Coq Verified Extraction plugin for Coq 8.19, available as source and through Coq’s opam archive. This plugin builds on MetaCoq’s verified erasure and provides an alternative, verified extraction plugin to OCaml/malfunction. It produces untyped malfunction programs and typed interface files that can be further compiled using the malfunction/OCaml compil...
Discourse Bot (Aug 07 2024 at 13:16):@rtetley (Romain Tetley) posted in [VsCoq 2] Release 2.1.7
Hi everyone,
We are pleased to announce the next release of VsCoq. This release covers a number of fixes and new features. Some of these features were added in pre-releases (2.1.5, and 2.1.6) which we summarise here:v2.1.5
Capabilities for quickfixes
[quickfix]
We have worked on adding quickfixes to VsCoq. However this relies on a change in the Coq API (which should send quickfix suggest...
Discourse Bot (Aug 19 2024 at 16:25):@bacam (Brian Campbell) posted in Big Specification workshop at the Newton Institute
As part of an Isaac Newton Institute programme on Big Specification, a workshop is being organised on:
Big Specification: Specification, Proof, and Testing at ScaleDate: 7-11 October 2024
Location: the Isaac Newton Institute, Cambridge, UK
Register at: https://www.newton.ac.uk/event/bspw01/
Deadline: 31 Aug 2024Tentative schedule:
Monday 7 OctoberTime
Title9:30 - 10:00
registrati...
Discourse Bot (Sep 11 2024 at 07:56):@proux01 (Pierre Roux) posted in Coq 8.20.0 is out
We are proud to announce the immediate availability of Coq 8.20. This
version adds a new rewrite rule mechanism along with a few new
features, a host of improvements to the virtual machine, the notation
system, Ltac2 and the standard library. This release has been made
possible thanks to the work of dozens of contributors and reviewers,
see the [changelog](Recent changes — Coq 8.20.0 document...
Discourse Bot (Sep 14 2024 at 09:44):@rtetley (Romain Tetley) posted in [VsCoq 2] Release 2.2.0
Hi everyone,
We are pleased to announce the next release of VsCoq. You can find a nicely formatted changelog here:We would like to thank the Coq core developers as well as TDiazT (Tomás Díaz) · GitHub and Durbatuluk1701 (Will Thomas) · GitHub for their contributions to this release !
Stay tuned for more improvements !
Romain, for the VsCoq team.
Discourse Bot (Sep 16 2024 at 15:07):@rtetley (Romain Tetley) posted in [Job Offer] Production Engineer for the Coq Platform
Dear Coq Community,
We are opening an engineering position at the Inria University Côte d’Azur center.
In short, your main job would be to handle the production of the Coq Platform. See full details here.
Please forward this advertisement to any interested individual, and address any questions to:
romain.tetley@inria.fr
Romain
Discourse Bot (Sep 18 2024 at 11:48):@pi8027 (Kazuhiko Sakaguchi) posted in Sixth Mathcomp sharing day
Dear Rocq/Coq and Mathematical components library users, we are pleased to announce our sixth “Mathcomp sharing day”. On September 25th 2024, From 9am to 5pm Paris time, mathcomp users, from enthusiasts to experts, are welcome to casually meetup online and engage in various activity from contributing to mathcomp (fixing bugs, solving issues, adding features, integrating external developments to ma...
Discourse Bot (Sep 22 2024 at 10:17):@Sebastian_Ullrich posted in [WITS 2025] Call for Contributions: 4th Workshop on the Implementation of Type Systems
WITS 2025 is the fourth Workshop on the Implementation of Type Systems. The
workshop will be held on January 25, 2025, in Denver, USA, co-located
with POPL. The goal of this workshop is to bring together the implementors of a
variety of languages with advanced type systems. The main focus is on the
practical issues that come up in the implementation of these systems, rather
than the theoretic...
Discourse Bot (Sep 24 2024 at 06:21):@rtetley (Romain Tetley) posted in [VsCoq 2] Release 2.2.1
Hi everyone,
We are pleased to announce the next release of VsCoq.
You can find a detailed change log here:Thanks to Durbatuluk1701 (Will Thomas) · GitHub for his contributions !
Stay tuned for more improvements !
Romain, for the VsCoq team
Discourse Bot (Sep 30 2024 at 18:20):@caverill (Charles Averill) posted in Proofchat: A TCP client/server chat application written in Coq
Hi all. I just got through writing:
A chat application written in Coq that utilizes extraction facilities and RecDef to generate performant OCaml networking code.
[screenshot]
This was a fun experiment and I encountered a ton of quirks regarding extraction that I hadn’t encountered before. I’m likely going to put together a document covering all of the challenges I encountered, hopefully it c...
Discourse Bot (Oct 03 2024 at 08:45):@CohenCyril (Cyril Cohen) posted in [Postdoc position] Machine Learning for translation between formal mathematics libraries (2nd announcement)
Dear proof assistant users,
I would like to advertise an open position at ENS Lyon on the translation between formal mathematics libraries using machine learning techniques.
The purpose of this postdoc is to experiment with both open-weight and closed-weight models to evaluate how LLMs can help bridge gaps between mathematical libraries of different proof assistants, and is a part of larger proj...
Last updated: Oct 13 2024 at 01:02 UTC