Meta Linear Logical Framework

被引：1
|
作者：
McCreight, Andrew [1 ]
Schuermann, Carsten [1 ]
机构：
[1] Yale Univ, New Haven, CT 06520 USA
来源：
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2008年 / 199卷
关键词：
Logical framework; meta language; meta logic; L-omega(+); linear logical framework;
D O I：
10.1016/j.entcs.2007.11.016
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Logical frameworks serve as meta languages to represent deductive systems, sometimes requiring special purpose meta logics to reason about the representations. In this work, we describe L-omega(+), a meta logic for the linear logical framework LLF [6] and illustrate its use via a proof of the admissibility of cut in the sequent calculus for the tensor fragment of linear logic. L-omega(+). is first-order, intuitionistic, and not linear. The soundness of L-omega(+) is shown.
引用
收藏
页码：129 / 147
页数：19
相关论文
共 50 条
  • [1] A linear logical framework
    Cervesato, I
    Pfenning, F
    [J]. INFORMATION AND COMPUTATION, 2002, 179 (01) : 19 - 75
  • [2] A linear logical framework
    Cervesato, I
    Pfenning, F
    [J]. 11TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1996, : 264 - 275
  • [3] A Fresh View of Linear Logic as a Logical Framework
    Olarte, Carlos
    Pimentel, Elaine
    Xavier, Bruno
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2020, 351 : 143 - 165
  • [4] A fresh view of linear logic as a logical framework
    Pimentel, Elaine
    [J]. Electronic Proceedings in Theoretical Computer Science, EPTCS, 2021, 332
  • [5] A Linear Logical Framework in Hybrid (Invited Talk)
    Felty, Amy P.
    [J]. PROCEEDINGS OF THE 8TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP' 19), 2019, : 14 - 14
  • [6] LINCX: A Linear Logical Framework with First-Class Contexts
    Georges, Aina Linn
    Murawska, Agata
    Otis, Shawn
    Pientka, Brigitte
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS (ESOP 2017): 26TH EUROPEAN SYMPOSIUM ON PROGRAMMING, 2017, 10201 : 530 - 555
  • [7] Logical Relations for a Logical Framework
    Rabe, Florian
    Sojakova, Kristina
    [J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2013, 14 (04)
  • [8] A logical framework
    Nancholas, S
    [J]. HEALTH POLICY AND PLANNING, 1998, 13 (02) : 189 - 193
  • [9] A focused linear logical framework and its application to metatheory of object logics
    Felty, Amy
    Olarte, Carlos
    Xavier, Bruno
    [J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2021, 31 (03) : 312 - 340
  • [10] Twelf and delphin:: Logic and functional programming in a meta-logical framework
    Schürmann, C
    [J]. FUNCTIONAL AND LOGIC PROGRAMMING, 2004, 2998 : 22 - 23
12345