Higher-order Representation of Substructural Logics

被引：0
|
作者：
Crary, Karl [1 ]
机构：
[1] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA
来源：
ICFP 2010: PROCEEDINGS OF THE 2010 ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING | 2010年
关键词：
Logical frameworks; linear logic; modal logic; mechanized metatheory;
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We present a technique for higher-order representation of substructural logics such as linear or modal logic. We show that such logics can be encoded in the (ordinary) Logical Framework, without any linear or modal extensions. Using this encoding, metatheoretic proofs about such logics can easily be developed in the Twelf proof assistant.
引用
收藏
页码：131 / 141
页数：11
相关论文
共 50 条
12345