Some Domain Theory and Denotational Semantics in Coq

Some Domain Theory and Denotational Semantics in Coq
复制标题

Coq 中的一些领域理论和指称语义

DOI：
10.1007/978-3-642-03359-9_10
复制
发表时间：
2009
期刊：
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
通讯作者：
C. Varming
C. Varming
中科院分区：
--
文献类型：
--
作者：
Nick Benton;A. Kennedy;C. Varming

文献摘要

被引文献

相似文献

我们提出了一个Coq形式化的建设性 *-CPOS（Paulin-Mohring的早期工作的扩展），并包括逆极限的混合方差递归域方程的解决方案的建设，以及这些解决方案的不变关系的存在。然后，我们定义了操作和指称语义的简单类型的CBV语言与递归和无类型的CBV语言，并建立健全和充分的结果在每种情况下。
We present a Coq formalization of constructive *** -cpos (extending earlier work by Paulin-Mohring) up to and including the inverse-limit construction of solutions to mixed-variance recursive domain equations, and the existence of invariant relations on those solutions. We then define operational and denotational semantics for both a simply-typed CBV language with recursion and an untyped CBV language, and establish soundness and adequacy results in each case.