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.
J-Calc : a Typed Lambda Calculus for Intuitionistic Justification Logic / K. Pouliasis, G. Primiero. - In: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE. - ISSN 1571-0661. - 300:(2014), pp. 71-87. [10.1016/j.entcs.2013.12.012]
J-Calc : a Typed Lambda Calculus for Intuitionistic Justification Logic
G. Primiero
2014
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.
| File | Dimensione | Formato | |
|---|---|---|---|
|
1-s2.0-S1571066113000923-main (2).pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
271.88 kB
Formato
Adobe PDF
|
271.88 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
