We describe a new approach to automatically repairing broken proofs in the Coq proof assistant in response to changes in types. Our approach combines a configurable proof term transformation with a decompiler from proof terms to tactic scripts. The proof term transformation implements transport across equivalences in a way that removes references to the old version of the changed type and does not rely on axioms beyond those Coq assumes. We have implemented this approach in PUMPKIN Pi, an extension to the PUMPKIN PATCH Coq plugin suite for proof repair. We demonstrate PUMPKIN Pi's flexibility on eight case studies, including supporting a benchmark from a user study, easing development with dependent types, porting functions and proofs between unary and binary numbers, and supporting an industrial proof engineer to interoperate between Coq and other verification tools more easily.
翻译：我们描述一种针对类型变化自动修复 Coq 校对助理的破损证明的新方法。 我们的方法将一个可配置的证明术语转换与一个从验证术语到战术脚本的分解器结合起来。 校对术语转换可以将旧版本的修改型号的参考去除,而不依赖这些 Coq 假设之外的轴承。 我们在PUMPKIN Pi 中采用了这一方法, 将PUMPKIN Patch Coq 插件套件套件的扩展用于证据修复。 我们在八个案例研究中展示了 PUMPKIN Pi 的灵活性, 包括支持用户研究的基准, 缓解依赖型号的开发, 单数和二数之间的移植功能和证明, 支持工业验证工程师在Coq 和其他核查工具之间更容易地进行操作 。
相关内容
- Today (iOS and OS X): widgets for the Today view of Notification Center
- Share (iOS and OS X): post content to web services or share content with others
- Actions (iOS and OS X): app extensions to view or manipulate inside another app
- Photo Editing (iOS): edit a photo or video in Apple's Photos app with extensions from a third-party apps
- Finder Sync (OS X): remote file storage in the Finder with support for Finder content annotation
- Storage Provider (iOS): an interface between files inside an app and other apps on a user's device
- Custom Keyboard (iOS): system-wide alternative keyboards
Source: iOS 8 Extensions: Apple’s Plan for a Powerful App Ecosystem
微信扫码咨询专知VIP会员