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 条
12345