Towards user-friendliness in proof assistants: automated strategies algebraic effects and handlers
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 - 11:20|
|11:20 - 11:40|
April GonçalvesMetastate AGPre-print
|11:40 - 12:00|
Alastair ReidArm Ltd, Luke ChurchUniversity of Cambridge, Shaked FlurGoogle Research, Sarah de HaasGoogle Research, Maritza JohnsonGoogle Research, Ben LaurieGoogle ResearchLink to publication