SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Wed 18 Nov 2020 11:20 - 11:40 at SPLASH-IV - Formal Methods Chair(s): Michael Coblenz

Proof assistants provide a framework for the modelling and verification of theories, as well as trustworthy software. However, such power is usually only available to experts. We propose a new approach, based on algebraic effects and handlers, to integrate different automated proof strategies that enable newcomers to take advantage of proof assistants without an in-depth understanding of underlying theory. Our approach gives newcomers an effect system, a handful of effectful strategies (tactics, proof search, and SMT solvers) and their handlers under a shared interface, while advanced users can extend our system with new effects and new handlers. Lastly, we prototype the system as a library in Agda. While our prototype is minimal, it shows how easily proofs can be carried out so long as the user has the correct intuition. We believe our system empowers non-experts and has the potential to bring verified software to relevant industries, such as finance.

Wed 18 Nov
Times are displayed in time zone: Central Time (US & Canada) change

11:00 - 12:20: Formal MethodsHATRA at SPLASH-IV
Chair(s): Michael CoblenzUniversity of Maryland at College Park
11:00 - 11:20
Meeting
HATRA
11:20 - 11:40
Talk
HATRA
April GonçalvesMetastate AG
Pre-print
11:40 - 12:00
Talk
HATRA
Alastair ReidArm Ltd, Luke ChurchUniversity of Cambridge, Shaked FlurGoogle Research, Sarah de HaasGoogle Research, Maritza JohnsonGoogle Research, Ben LaurieGoogle Research
Link to publication