A Functorial Bridge Between the Infinitary Affine Lambda-Calculus and Linear Logic

被引:0
作者
Mazza, Damiano [1 ]
Pellissier, Luc [1 ]
机构
[1] Univ Paris 13, Sorbonne Paris Cite, LIPN, CNRS,UMR 7030, F-93430 Villetaneuse, France
来源
THEORETICAL ASPECTS OF COMPUTING - ICTAC 2015 | 2015年 / 9399卷
关键词
D O I
10.1007/978-3-319-25150-9_10
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
It is a well known intuition that the exponential modality of linear logic may be seen as a form of limit. Recently, Mellies, Tabareau and Tasson gave a categorical account for this intuition, whereas the first author provided a topological account, based on an infinitary syntax. We relate these two different views by giving a categorical version of the topological construction, yielding two benefits: on the one hand, we obtain canonical models of the infinitary affine lambda-calculus introduced by the first author; on the other hand, we find an alternative formula for computing free commutative comonoids in models of linear logic with respect to the one presented by Mellies et al.
引用
收藏
页码:144 / 161
页数:18
相关论文
共 12 条
[1]  
Abramsky S, 2000, INFORM COMPUT, V163, P409, DOI [10.1006/inco.2000.2930, 10.1006/inco2000.2930]
[2]  
Benton P.N., 1993, P TLCA, P75
[3]  
Curien P.L., 2009, INTERACTIVE MODELS C
[4]   Finiteness spaces [J].
Ehrhard, T .
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2005, 15 (04) :615-646
[5]   LINEAR LOGIC [J].
GIRARD, JY .
THEORETICAL COMPUTER SCIENCE, 1987, 50 (01) :1-102
[6]   A linearization of the lambda-calculus and consequences [J].
Kfoury, AJ .
JOURNAL OF LOGIC AND COMPUTATION, 2000, 10 (03) :411-436
[7]  
Mac Lane S., 1978, CATEGORIES WORKING M, DOI [10.1007/978-1-4757-4721-8, DOI 10.1007/978-1-4757-4721-8]
[8]   CATEGORICAL ALGEBRA [J].
MACLANE, S .
BULLETIN OF THE AMERICAN MATHEMATICAL SOCIETY, 1965, 71 (01) :40-+
[9]   An Infinitary Affine Lambda-Calculus Isomorphic to the Full Lambda-Calculus [J].
Mazza, Damiano .
2012 27TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2012, :471-480
[10]  
Mellies P.-A., 2004, PPS040631