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+i...@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 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
