J-Calc: A Typed Lambda Calculus for Intuitionistic Justification Logic

被引：1

作者：

Pouliasis, Konstantinos ^{[1
]}

Primiero, Giuseppe ^{[2
]}

机构：

[1] CUNY, Grad Ctr, Dept Comp Sci, New York, NY USA

[2] Middlesex Univ, Dept Comp Sci, London, England

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2014年 / 300卷

关键词：

Typed lambda-calculus; Justification Logic; Modular Programming;

D O I：

10.1016/j.entcs.2013.12.012

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

In this paper we offer a system J-Calc that can be regarded as a typed lambda-calculus for the {->, perpendicular to} fragment of Intuitionistic Justification Logic. We offer different interpretations of J-Calc, in particular, as a two phase proof system in which we proof check the validity of deductions of a theory T based on deductions from a stronger theory T' and computationally as a type system for separate compilations. We establish some first metatheoretic results.

引用

页码：71 / 87

页数：17

共 50 条

[1] Lambda calculus and intuitionistic linear logic
Rocca S.R.D.
Roversi L.
Studia Logica, 1997, 59 (3) : 417 - 448
[2] STRONG NORMALIZATION OF A TYPED LAMBDA CALCULUS FOR INTUITIONISTIC BOUNDED LINEAR-TIME TEMPORAL LOGIC
Kamide, Norihiro
REPORTS ON MATHEMATICAL LOGIC, 2012, 47 : 29 - 61
[3] Propositions with Typed Lambda Calculus λ
Singh H.
SN Computer Science, 2022, 3 (3)
[4] HTLC: Hyperintensional typed Lambda calculus
Fait, Michal
Primiero, Giuseppe
Journal of Applied Logics, 2021, 8 (02): : 469 - 495
[5] HTLC: HYPERINTENSIONAL TYPED LAMBDA CALCULUS
Fait, Michal
Primiero, Giuseppe
JOURNAL OF APPLIED LOGICS-IFCOLOG JOURNAL OF LOGICS AND THEIR APPLICATIONS, 2021, 8 (02): : 469 - 495
[6] A typed lambda calculus with intersection types
Bono, Viviana
Venneri, Betti
Bettini, Lorenzo
THEORETICAL COMPUTER SCIENCE, 2008, 398 (1-3) : 95 - 113
[7] Atomic lambda-calculus: a typed lambda-calculus with explicit sharing
Gundersen, Tom
Heijltjes, Willem
Parigot, Michel
2013 28TH ANNUAL IEEE/ACM SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2013, : 311 - 320
[8] TYPED LAMBDA-CALCULUS WITH RECURSIVE DEFINITIONS
KOTOV, SV
LECTURE NOTES IN COMPUTER SCIENCE, 1992, 620 : 246 - 257
[9] Semantics of a Typed Algebraic Lambda-Calculus
Valiron, Benoit
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2010, (26): : 147 - 158
[10] Normalization by evaluation for typed lambda calculus with coproducts
Altenkirch, T
Dybjer, P
Hofmann, M
Scott, P
16TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2001, : 303 - 310

← 1 2 3 4 5 →