Abstract types have existential types

Abstract types have existential types
复制标题

抽象类型具有存在类型

DOI：
--
复制
发表时间：
1985
期刊：
ACM-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
通讯作者：
G. Plotkin
G. Plotkin
中科院分区：
--
文献类型：
--
作者：
John C. Mitchell;G. Plotkin

文献摘要

被引文献

相似文献

数据类型声明出现在诸如Ada、Alphard、CLU和ML等有类型编程语言中。这种声明形式将一列标识符绑定到一个带有相关操作的类型上，这是一个复合“值”，我们称之为数据代数。我们使用二阶有类型λ演算SOL来展示如何给数据代数赋予类型、将其作为参数传递以及作为函数调用的结果返回。在此过程中，我们讨论抽象数据类型声明的语义，并回顾有类型编程语言与构造性逻辑之间的联系。
data type declarations appear in typed programming languages like Ada, Alphard, CLU and ML. This form of declaration binds a list of identifiers to a type with associated operations, a composite "value" we call a data algebra. We use a second-order typed lambda calculus SOL to show how data algebras may be given types, passed as parameters, and returned as results of function calls. In the process, we discuss the semantics of abstract data type declarations and review a connection between typed programming languages and constructive logic.