用于程序和证明重用的零成本强制
Zero-Cost Coercions for Program and Proof Reuse
摘要：
我们引入的概念之间的非索引和索引的归纳数据库的变体，如列表和向量的身份识别。标识强制将一种类型转换为另一种类型，使得强制函数在定义上简化为标识函数。这允许我们重用向量程序来派生列表程序（反之亦然），而没有任何运行时成本。这也允许我们重用向量证明来导出列表证明（反之亦然），而无需等式推理证明义务。我们的工作是形式化的Cedille，依赖类型的程序设计语言的基础上的类型注释的Curry风格的类型理论与隐式（或擦除）产品（或，依赖函数），并依赖擦除引入定义之间的基本非类型化条款的平等。
英文摘要：
We introduce the notion of identity coercions between non-indexed and indexed variants of inductive datatypes, such as lists and vectors. An identity coercion translates one type to another such that the coercion function definitionally reduces to the identity function. This allows us to reuse vector programs to derive list programs (and vice versa), without any runtime cost. This also allows us to reuse vector proofs to derive list proofs (and vice versa), without the cost of equational reasoning proof obligations. Our work is formalized in Cedille, a dependently typed programming language based on a type-annotated Curry-style type the- ory with implicit (or, erased) products (or, dependent functions), and relies crucially on erasure to introduce definitional equalities between underlying untyped terms.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
