期刊
ACM TRANSACTIONS ON COMPUTATIONAL LOGIC
卷 9, 期 3, 页码 -出版社
ASSOC COMPUTING MACHINERY
DOI: 10.1145/1352582.1352591
关键词
design; theory; type theory; logical frameworks; intuitionistic modal logic
The intuitionistic modal logic of necessity is based on the judgmental notion of categorical truth. In this article we investigate the consequences of relativizing these concepts to explicitly specified contexts. We obtain contextual modal logic and its type-theoretic analogue. Contextual modal type theory provides an elegant, uniform foundation for understanding metavariables and explicit substitutions. We sketch some applications in functional programming and logical frameworks.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据