Multiplexor categories and models of soft linear logic

被引:4
作者
Redmond, Brian F. [1 ]
机构
[1] Univ Ottawa, Dept Math & Stat, Ottawa, ON K1N 6N5, Canada
来源
LOGICAL FOUNDATIONS OF COMPUTER SCIENCE, PROCEEDINGS | 2007年 / 4514卷
关键词
D O I
10.1007/978-3-540-72734-7_33
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We give a categorical interpretation of Lafont's Soft Linear Logic, a logical system complete for polynomial time computation, in terms of multiplexor categories. We present two main classes of models and methods for constructing examples in each case. As a concrete example of the first type, we introduce a simple game semantics for Multiplicative Soft Linear Logic. To illustrate the second type, we give a realizability model and a new proof of the polytime soundness of Soft Linear Logic. These results further our semantic understanding of Soft Linear Logic and polynomial time.
引用
收藏
页码:472 / 485
页数:14
相关论文
共 15 条
[1]  
ABRAMSKY S, 2002, CLIFFORD LECT
[2]  
Abramsky S., 1997, Proceedings of the 1996 CLiCS Summer School, Isaac Newton Institute, P1
[3]   Stratified coherence spaces: a denotational semantics for light linear logic [J].
Baillot, P .
THEORETICAL COMPUTER SCIENCE, 2004, 318 (1-2) :29-55
[4]  
Bierman G. M., 1995, LECT NOTES COMPUTER, V902, P78
[5]  
Dal Lago U, 2005, LECT NOTES COMPUT SC, V3821, P189, DOI 10.1007/11590156_15
[6]   BOUNDED LINEAR LOGIC - A MODULAR APPROACH TO POLYNOMIAL-TIME COMPUTABILITY [J].
GIRARD, JY ;
SCEDROV, A ;
SCOTT, PJ .
THEORETICAL COMPUTER SCIENCE, 1992, 97 (01) :1-66
[7]   LINEAR LOGIC [J].
GIRARD, JY .
THEORETICAL COMPUTER SCIENCE, 1987, 50 (01) :1-102
[8]   Light linear logic [J].
Girard, JY .
INFORMATION AND COMPUTATION, 1998, 143 (02) :175-204
[9]  
Hofmann M, 2004, THEOR COMPUT SCI, V318, P121, DOI [10.1016/j.tcs.2003.10.019, 10.1016/j.tcs.203.10.019]
[10]   Soft linear logic and polynomial time [J].
Lafont, Y .
THEORETICAL COMPUTER SCIENCE, 2004, 318 (1-2) :163-180