Intuitionistic Hypothetical Logic of Proofs

Gabriela Steren, Eduardo Bonelli

Research output: Contribution to journalArticlepeer-review

5 Scopus citations

Abstract

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 λIHLP. 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.

Original languageEnglish
Pages (from-to)89-103
Number of pages15
JournalElectronic Notes in Theoretical Computer Science
Volume300
DOIs
StatePublished - 21 Jan 2014

Keywords

  • Curry-Howard
  • Lambda Calculus
  • Logic of Proofs
  • Programming Languages

Fingerprint

Dive into the research topics of 'Intuitionistic Hypothetical Logic of Proofs'. Together they form a unique fingerprint.

Cite this