Coq中的Gradual Certified Programming
Gradual Certified Programming in Coq
摘要：
表达性的静态类型规则是实现高质量软件的一种强有力的方法。然而，不应低估采用这些技术的成本。就像渐进式类型允许从动态类型到静态类型的程序的平滑过渡一样，支持渐进式路径到认证编程似乎是可取的。我们探索逐步认证的编程在Coq，提供了可能性，推迟选定的属性的证明，并检查“在运行时”是否属性实际上举行。强制转换可以与Coq的隐式强制机制集成，以支持隐式强制转换插入（渐进类型化）。此外，当将Coq函数提取到主流语言时，我们的强制转换编码支持将假定的属性提升到运行时检查中。令我们惊讶的是，没有必要以任何方式扩展Coq来支持渐进式认证编程。类型类和公理的简单混合使得以简单的方式将渐进认证编程引入Coq成为可能。
英文摘要：
Expressive static typing disciplines are a powerful way to achieve high-quality software. However, the adoption cost of such techniques should not be under-estimated. Just like gradual typing allows for a smooth transition from dynamically-typed to statically-typed programs, it seems desirable to support a gradual path to certified programming. We explore gradual certified programming in Coq, providing the possibility to postpone the proofs of selected properties, and to check "at runtime" whether the properties actually hold. Casts can be integrated with the implicit coercion mechanism of Coq to support implicit cast insertion a la gradual typing. Additionally, when extracting Coq functions to mainstream languages, our encoding of casts supports lifting assumed properties into runtime checks. Much to our surprise, it is not necessary to extend Coq in any way to support gradual certified programming. A simple mix of type classes and axioms makes it possible to bring gradual certified programming to Coq in a straightforward manner.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
