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