Intuitionistic Hypothetical Logic of Proofs
| Autor: | Eduardo Bonelli, Gabriela Steren |
|---|---|
| Jazyk: | angličtina |
| Předmět: |
Discrete mathematics
Natural deduction General Computer Science Modal logic Curry-Howard Term (logic) Mathematical proof Curry–Howard correspondence Theoretical Computer Science Ciencias de la Computación TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Fragment (logic) Ciencias de la Computación e Información TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Logic of Proofs Calculus Programming Languages Lambda Calculus Lambda calculus Typed lambda calculus computer CIENCIAS NATURALES Y EXACTAS Mathematics computer.programming_language Computer Science(all) |
| Zdroj: | Electronic Notes in Theoretical Computer Science. :89-103 |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/j.entcs.2013.12.013 |
| Popis: | 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. Fil: Steren, Gabriela. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentina Fil: Bonelli, Eduardo Augusto. Universidad Nacional de Quilmes. Departamento de Ciencia y Tecnología; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|