Static and user-extensible proof checking

11 years 11 months ago

Download zoo.cs.yale.edu

Despite recent successes, large-scale proof development within proof assistants remains an arcane art that is extremely timeconsuming. We argue that this can be attributed to two profound shortcomings in the architecture of modern proof assistants. The ﬁrst 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-speciﬁc 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 typesafe 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...

Antonis Stampoulis, Zhong Shao

Real-time Traffic