Proof systems have been used as constructive demonstrations of mathematical validity for millennia, and are now being implemented on computers as "formal proofs". They enable very high levels of reliability as they are reproducible, objective and verifiable.
Formal proof systems capture the definitions, statements and proofs of mathematical discourse using precisely defined formal languages and rules of inference. Proof technology can be used to perform large calculations reliably, solve systems of constraints, discover and visualise examples and counter examples, simplify expressions, explore hypotheses, navigate large libraries of mathematical knowledge and capture abstractions and patterns of reasoning. Importantly, such technologies can transform mathematical practice across a range of scientific and engineering disciplines. They are essential for instance, in the context of hardware and software systems where formal verification is needed to prove the correctness, security and safety of designs, as well as the algorithms and implementations which underpin a system specification.
This workshop, part of the Isaac Newton Institute Research Programme Big Proof, will bring together mathematicians, computer scientists and logicians with those from relevant application areas, to explore the foundational, theoretical, and practical challenges in exploiting proof technology. A key expected output is a concrete, long-term research agenda for making computational inference a basic technology for formalising, creating, curating and disseminating mathematical knowledge in digital form.
Aims and Objectives
The aim of the workshop is to promote discussion around the area of big proof and formal verification, and the challenges from academic and industry perspectives. For example, academic challenges are presented by the problem of scaling mathematical proof on machine, including issues such as search, representation and reasoning in ways that are more natural to working mathematicians than current systems offer. Conversely, industry challenges may be posed around the limits of automation and the efficiency of current logics and algorithms.
The Programme of talks will feature both academic and industry speakers and will include areas such as:
- Verification for mainstream software and security
- Bringing big verification proof to big finance
- Big proofs from social networks of mathematics
- Reasoning with big code
- Reasoning at scale for cloud computing security
A key aspect of the workshop will be to encourage links between academics and industry and allow both parties to further understand the others’ needs. Therefore, as well as highlighting state-of-the-art mathematics for formal proof systems, talks will also cover end user challenges and experiences. Discussion and networking sessions will allow for new research directions to be discussed and areas of mutual interest to be explored.
Registration and Venue
This workshop will be of interest to individuals from research, business and industry communities, who are interested in areas of big proof and formal verification. Relevant sectors include engineering, computer hardware and software, security and finance.
Please use this link to register your place.
There is a nominal registration fee of £50.00 for non-academics to cover refreshments and administration.
Non-academic registrations will then be sent a payment link to pay the registration fee.
The workshop will take place at the Alan Turing Institute, London. The Institute is headquartered at the British Library.
Please see the link for directions to the venue.