J-Calc: a typed lambda calculus for intuitionistic justification logic

Article


Pouliasis, K. and Primiero, G. 2014. J-Calc: a typed lambda calculus for intuitionistic justification logic. Electronic Notes in Theoretical Computer Science. 300, pp. 71-87. https://doi.org/10.1016/j.entcs.2013.12.012
TypeArticle
TitleJ-Calc: a typed lambda calculus for intuitionistic justification logic
AuthorsPouliasis, K. and Primiero, G.
Abstract

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

Research GroupFoundations of Computing group
PublisherElsevier
JournalElectronic Notes in Theoretical Computer Science
ISSN1571-0661
Publication dates
Print21 Jan 2014
Online09 Jan 2014
Publication process dates
Deposited28 Nov 2014
Output statusPublished
Digital Object Identifier (DOI)https://doi.org/10.1016/j.entcs.2013.12.012
LanguageEnglish
First submitted version
Permalink -

https://repository.mdx.ac.uk/item/84y2v

Download files

  • 24
    total views
  • 3
    total downloads
  • 0
    views this month
  • 1
    downloads this month

Export as