The Coq mailing list

[Alex J Best <alex.j.best AT gmail.com>]

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, but we will review and
accept abstracts on a rolling basis before then. Please send abstracts
via email to alexjbest+icms AT gmail.com.

We hope to inspire people to bring both their completed projects but
also works in progress and demos to meet and discuss the intersections
of formal and informal mathematical software with a wide range of
interested participants. Abstracts will be published on the website
https://proof-assistants-and-software-icms2024.github.io/ as they are
accepted.

We welcome expressions of interest before the official deadline, both
of potential speakers and other participants in order to help us with
the planning.

There will be the opportunity for accepted speakers to publish
extended abstracts / papers in the proceedings of the ICMS, subject to
participant interest.
So if you have some work you'd like to present that would be of
interest for this session please submit an abstract to us whenever it
is ready!
For funding and other particulars about the ICMS and location and
travel please see the main ICMS website (which will be updated further
in future).

The full description of the session is as follows:
Interactive proof assistants (ITPs) are pieces of software that allow
one to express mathematical constructs and arguments and check them
interactively. Formalisation, the process of writing mathematical
proofs in these systems, is becoming increasingly popular amongst
mathematicians.

This session will showcase projects bridging the gap between ITPs and
other kinds of mathematical software and computation. There are many
aspects of this which could be explored further. For example; tactics
for ITPs which make use (and verify) witnesses extracted from
unverified computation; code extraction, allowing formalised
algorithms to be used for computer algebra; proof discovery and
visualisation tools within ITPs which make use of external
mathematical software; using proof assistants to check key reductions
in computer algebra; or interfaces between ITPs and SAT/SMT solvers to
verify completely automated proofs.

We hope that this session will foster collaboration among people
working in formalisation, computer algebra, and other areas of
mathematical computation.

Alex Best and Heather Macbeth