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.
A short abstract will appear on the permanent conference web page (see below) as soon as accepted.
An extended abstract may be submitted for the conference proceedings that will be distributed during the meeting.
A **journal special issue **consisting of full papers will be organized immediately after the meeting.
If you would like to give a talk at ICMS, you need to submit first a short abstract and then later an extended abstract. See the guidelines for the details.
After the meeting, the submission guideline for a journal special issue will be communicated to you by the session organizers.
© 2023. All rights reserved.
