Lambda World 2018 - How to make ad hoc proof automation less ad hoc - Aleksandar Nanevski35:04 398 views 100% Published 3 years ago
This presentation by Aleksandar Nanevski took place at Lambda World Cádiz on October 26th, 2018 at the Palacio de Congresos in Cádiz, Spain.
How to make ad hoc proof automation less ad hoc
To overcome the burden involved in interactively mechanizing mathematical proofs on a computer, most theorem-proving systems such as Coq and Isabelle, support user-customizable proof automation by means of tactics.
Tactics, introduced by Milner in Edinburgh LCF, are programs that can inspect and algorithmically manipulate assertions in the prover's base logic, with the goal of simplifying or discharging them.
While tactics are clearly useful in practice, they are beset by a number of fundamental limitations. They are written in a domain-specific scripting language, which by necessity resides outside of the prover's base logic, and lacks the base logic's precise typing. This in turn makes tactics famously difficult to maintain, and impossible to precisely specify and verify.
In this talk I will present an alternative architecture for user-customizable proof automation, specifically in Coq, which overcomes the above limitation.
The starting point is the observation, well known as Curry-Howard isomorphism, that proofs and programs in Coq are equivalent entities. Thus, concepts and ideas developed in the world of programming, can be applied to mathematics as well.
In particular, I will show how the idea of overloading a method name in programming (a.k.a. ad hoc polymorphism, static dispatch), can be applied to mathematical theorems.
Such an 'overloaded theorem' realizes a method for an automated discharge of a class of proof obligations, which, unlike a tactic, can itself be verified in the base logic of Coq, and flexibly composed with other Coq programs, theorems and proofs.
This is joint work with Georges Gonthier, Beta Ziliani and Derek Dreyer.
-https://www.47deg.com/events for more details