# J-Calc: A typed lambda calculus for Intuitionistic Justification Logic

Title | J-Calc: A typed lambda calculus for Intuitionistic Justification Logic |

Publication Type | Journal Article |

Year of Publication | 2014 |

Authors | Pouliasis, K, Primiero, G |

Journal | Electronic Notes in Theoretical Computer Science |

Volume | 300 |

Pagination | 71–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. |

DOI | 10.1016/j.entcs.2013.12.012 |

Citation Key | pouliasis2014j |

PDF author (public):