Intuitionistic Hypothetical Logic of Proofs

Gabriela Steren; Eduardo Bonelli

doi:10.1016/j.entcs.2013.12.013

Intuitionistic Hypothetical Logic of Proofs

Gabriela Steren
, Eduardo Bonelli

Universidad de Buenos Aires

Research output: Contribution to journal › Article › peer-review

6 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 language	English
Pages (from-to)	89-103
Number of pages	15
Journal	Electronic Notes in Theoretical Computer Science
Volume	300
DOIs	https://doi.org/10.1016/j.entcs.2013.12.013
State	Published - 21 Jan 2014

Keywords

Curry-Howard
Lambda Calculus
Logic of Proofs
Programming Languages

Access to Document

10.1016/j.entcs.2013.12.013

Cite this

@article{398327ae048b4fb6a503c8acb562db22,

title = "Intuitionistic Hypothetical Logic of Proofs",

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 {\~a}€{\v s}s{\~a}€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.",

keywords = "Curry-Howard, Lambda Calculus, Logic of Proofs, Programming Languages",

author = "Gabriela Steren and Eduardo Bonelli",

year = "2014",

month = jan,

day = "21",

doi = "10.1016/j.entcs.2013.12.013",

language = "English",

volume = "300",

pages = "89--103",

}

TY - JOUR

T1 - Intuitionistic Hypothetical Logic of Proofs

AU - Steren, Gabriela

AU - Bonelli, Eduardo

PY - 2014/1/21

Y1 - 2014/1/21

N2 - 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.

AB - 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.

KW - Curry-Howard

KW - Lambda Calculus

KW - Logic of Proofs

KW - Programming Languages

UR - https://www.scopus.com/pages/publications/84892184983

UR - https://www.scopus.com/pages/publications/84892184983#tab=citedBy

U2 - 10.1016/j.entcs.2013.12.013

DO - 10.1016/j.entcs.2013.12.013

M3 - Article

AN - SCOPUS:84892184983

SN - 1571-0661

VL - 300

SP - 89

EP - 103

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -

Intuitionistic Hypothetical Logic of Proofs

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this