Intuitionistic Hypothetical Logic of Proofs

We study a term assignment for an intuitonistic fragment of the Logic of Proofs (LP). LP is a refinement of modal logic S4 in which the assertion □A is replaced by 〚s〛A whose intended reading is “s is a proof of A”. We first introduce a natural deduction presentation based on hypothetical judgements and then its term assignment, which yields a confluent and strongly normalising typed lambda calculus . This work is part of an ongoing effort towards reformulating LP in terms of hypothetical reasoning in order to explore its applications in programming languages.