Polytypic programming in COQ
Polytypic programming in COQ
复制标题
COQ 中的多型编程
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Arthur P. Hughes
中科院分区：
文献类型：
--
作者：
W. Verbruggen;Edsko de Vries;Arthur P. Hughes
我们的工作的目的是提供一个基础设施的形式证明通用Haskell风格的多型程序。为了实现这个目标，我们必须有一个多型编程的定义，它既完全形式化，又尽可能接近泛型Haskell中的定义。在本文中，我们展示了一个形式化的证明助理Coq的类型和长期专业化。我们对术语专门化的定义可以解释为术语专门化的结果具有由类型专门化计算的类型的形式证明。
The aim of our work is to provide an infrastructure for formal proofs over Generic Haskell-style polytypic programs. For this goal to succeed, we must have a definition of polytypic programming which is both fully formal and as close as possible to the definition in Generic Haskell. In this paper we show a formalization in the proof assistant Coq of type and term specialization. Our definition of term specialization can be interpreted as a formal proof that the result of term specialization has the type computed by type specialization.