The Type Theory of PL/CV3
The Type Theory of PL/CV3
复制标题
PL/CV3的类型论
DOI：
10.1145/357233.357238
复制
发表时间：
1984
期刊：
影响因子：
--
通讯作者：
Daniel R. Zlatin
中科院分区：
文献类型：
--
作者：
R. Constable;Daniel R. Zlatin
编程逻辑PL/CV 3基于数学类型的概念。我们提出了类型理论的核心，从该理论中可以推导出完整的程序验证和规范理论。虽然完整的理论被设计为可用的，但核心理论被选择为可分析的。本演示力求简洁而全面。最后一节包含一些示例，但这里的方法不是教程。关键词和短语：自动逻辑，程序验证，程序规范，编程语言的语义，类型理论，数学基础。
The programming logic PL/CV3 is based on the notion of a mathematical type. We present the core of the type theory, from which the full theory for program verification and specification can be derived. Whereas the full theory was designed to be useable, the core theory was selected to be analyzable. This presentation strives to be succinct yet thorough. The last section consists of examples, but the approach here is not tutorial. Key Words and phrases: automated logic, program verification, program specification, semantics of programming languages, type theory, foundations of mathematics.