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
| Type | Article |
|---|---|
| Title | J-Calc: a typed lambda calculus for intuitionistic justification logic |
| Authors | Pouliasis, 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 Group | Foundations of Computing group |
| Publisher | Elsevier |
| Journal | Electronic Notes in Theoretical Computer Science |
| ISSN | 1571-0661 |
| Publication dates | |
| 21 Jan 2014 | |
| Online | 09 Jan 2014 |
| Publication process dates | |
| Deposited | 28 Nov 2014 |
| Output status | Published |
| Digital Object Identifier (DOI) | https://doi.org/10.1016/j.entcs.2013.12.012 |
| Language | English |
| First submitted version |
Permalink -
https://repository.mdx.ac.uk/item/84y2v
Download files
125
total views31
total downloads3
views this month2
downloads this month