Email Gateway (Dec 19 2023 at 01:45): Email Gateway (Dec 19 2023 at 01:45):From: alex.j.best@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@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
Email Gateway (Dec 19 2023 at 11:24):From: Paul Jackson <Paul.Jackson@ed.ac.uk>
Hi Ramon,
did you see this?
Talking about CvxLean then would be good. However, would your Apple contract allow this? If not, I’d be prepared to step in and give the talk.
* Paul.
Last updated: Apr 29 2024 at 01:08 UTC