Electronic Notes in Theoretical Computer Science

TitleJ-Calc: A typed lambda calculus for Intuitionistic Justification Logic
Publication TypeJournal Article
Year of Publication2014
AuthorsPouliasis, K, Primiero, G
JournalElectronic Notes in Theoretical Computer Science
Volume300
Pagination71–87
Abstract

In this paper we offer a system J-Calc that can be regarded as a typed λ -calculus for the {→,&\#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 Τ' and computationally as a type system for separate compilations. We establish some first metatheoretic results.

DOI10.1016/j.entcs.2013.12.012
Citation Keypouliasis2014j
Download PDF (Author PDF)
PDF author (public):