Witnessing (Co)datatypes
Witnessing (Co)datatypes
复制标题
见证（Co）数据类型
DOI：
10.1007/978-3-662-46669-8_15
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Dmitriy Traytel
中科院分区：
文献类型：
--
作者：
Jasmin Christian Blanchette;Andrei Popescu;Dmitriy Traytel
数据库和代码库对于指定和推理（可能是无限的）计算过程很有用。Isabelle/HOL证明助手最近扩展了一个定义包，支持两者。我们描述了一个完整的程序，用于在一般的相互递归，嵌套的情况下，nonempiry证人是一个但书引入类型在高阶逻辑。
Datatypes and codatatypes are useful for specifying and reasoning about (possibly infinite) computational processes. The Isabelle/HOL proof assistant has recently been extended with a definitional package that supports both. We describe a complete procedure for deriving nonemptiness witnesses in the general mutually recursive, nested case—nonemptiness being a proviso for introducing types in higher-order logic.
登录
查看更多内容
具有交错归纳的a-演算的预测强归一化证明
DOI：
--
发表时间：
1999
期刊：
影响因子：
--
作者：
Andreas Abel
通讯作者：
Andreas Abel
简单类型理论的表述（伊莎贝尔）
DOI：
--
发表时间：
1990
期刊：
Conference on Computer Logic
影响因子：
--
作者：
Lawrence Charles Paulson
通讯作者：
Lawrence Charles Paulson
为什么我们不能在 HOL 中使用 SML 风格的数据类型声明
DOI：
10.1016/b978-0-444-89880-7.50042-5
发表时间：
1992
期刊：
J. Log. Comput.
影响因子：
--
作者：
Elsa L. Gunter
通讯作者：
Elsa L. Gunter
解析函子的两种应用
影响因子：
1.1
作者：
R. Hasegawa
通讯作者：
R. Hasegawa
感应式、共感应式和尖头式
DOI：
--
发表时间：
1996
期刊：
ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
Brian T. Howard
通讯作者：
Brian T. Howard