J-Calc: A Typed Lambda Calculus for Intuitionistic Justification Logic
Konstantinos Pouliasis, Giuseppe Primiero · Electronic Notes in Theoretical Computer Science · 2014
In this paper we offer a system J-Calc that can be regarded as a typed λ -calculus for the { → , ⊥ } 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.