@article {pouliasis2014j,
	title = {J-Calc: A typed lambda calculus for Intuitionistic Justification Logic},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {300},
	year = {2014},
	pages = {71{\textendash}87},
	abstract = {<p>In this paper we offer a system J-Calc that can be regarded as a typed λ -calculus for the {{\textrightarrow},\&amp;\#8869;} 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 Τ based on deductions from a stronger theory Τ{\textquoteright} and computationally as a type system for separate compilations. We establish some first metatheoretic results.</p>},
	doi = {10.1016/j.entcs.2013.12.012},
	author = {Pouliasis, Konstantinos and Primiero, Giuseppe}
}
