Authors
Antonis Stampoulis
Zhong Shao
Abstract
Despite recent successes, large-scale proof development
within proof assistants remains an arcane art that is
extremely time-consuming. We argue that this can be
attributed to two profound shortcomings in the architecture
of modern proof assistants. The first is that proofs need
to include a large amount of minute detail; this is due
to the rigidity of the proof checking process, which
cannot be extended with domain-specific knowledge.
In order to avoid these details, we rely on developing and using
tactics, specialized procedures that produce proofs. Unfortunately,
tactics are both hard to write and hard to use, revealing the
second shortcoming of modern proof assistants. This is because
there is no static knowledge about their expected use and behavior.
As has recently been demonstrated, languages that allow type-safe
manipulation of proofs, like Beluga, Delphin and VeriML, can be used
to partly mitigate this second issue, by assigning rich types to
tactics. Still, the architectural issues remain. In this paper, we
build on this existing work, and demonstrate two novel ideas: an
extensible conversion rule and support for static proof
scripts. Together, these ideas enable us to support both
user-extensible proof checking, and sophisticated static checking of
tactics, leading to a new point in the design space of future
proof assistants. Both ideas are based on the interplay between
a light-weight staging construct and the rich type information
available.
Published
In
Proc. 39th ACM Symposium on Principles of Programming
Languages (POPL'12), Philadelphia, PA,
pages 273-284, January 2012. ©2012 ACM.
- Paper (PDF)
- Extended TR (PDF)
- Implementation (zip)