Intuitionistic Hypothetical Logic of Proof

Volver a la Vista simple
dc.conicet.organizacionUniversidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación
dc.conicet.organizacionUniversidad Nacional de Quilmes. Departamento de Ciencia y Tecnología
dc.conicet.organizacionConsejo Nacional de Investigaciones Científicas y Técnicas
dc.conicet.paisOrganizacionArgentina
dc.conicet.paisOrganizacionArgentina
dc.conicet.paisOrganizacionArgentina
dc.conicet.produccionid5419357
dc.contributor.authorSteren, Gabriela
dc.contributor.authorBonelli, Eduardo Augusto
dc.date.accessioned2017-11-15T14:20:21Z
dc.date.available2017-11-15T14:20:21Z
dc.date.issued2013-10
dc.date.updated2017-11-15T14:10:19Z
dc.description.abstractWe 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.es
dc.description.filFil: Steren, Gabriela. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Computación; Argentina
dc.description.filFil: Bonelli, Eduardo Augusto. Universidad Nacional de Quilmes. Departamento de Ciencia y Tecnología; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina
dc.formatapplication/pdfes
dc.identifier.citationSteren, Gabriela; Bonelli, Eduardo Augusto; Intuitionistic Hypothetical Logic of Proof; Elsevier Science; Electronic Notes in Theoretical Computer Science; 300; 10-2013; 89-103es
dc.identifier.institucionalCONICET
dc.identifier.issn1571-0661es
dc.identifier.repoCONICET Digital
dc.identifier.urihttp://hdl.handle.net/11336/28208
dc.journal.ciudadAmsterdames
dc.journal.pagination89-103es
dc.journal.paisPaíses Bajoses
dc.journal.titleElectronic Notes in Theoretical Computer Sciencees
dc.journal.volume300es
dc.language.isoenges
dc.publisherElsevier Sciencees
dc.relation.alternativeidinfo:eu-repo/semantics/altIdentifier/doi/http://dx.doi.org/10.1016/j.entcs.2013.12.013
dc.relation.alternativeidinfo:eu-repo/semantics/altIdentifier/url/http://www.sciencedirect.com/science/article/pii/S1571066113000935
dc.rightsinfo:eu-repo/semantics/openAccess*
dc.rights.urihttps://creativecommons.org/licenses/by-nc-sa/2.5/ar/*
dc.subjectCurry-Howardes
dc.subjectLogic of Proofses
dc.subjectLambda Calculuses
dc.subjectProgramming Languageses
dc.subject.classificationCiencias de la Computaciónes
dc.subject.classificationCiencias de la Computación e Informaciónes
dc.subject.classificationCIENCIAS NATURALES Y EXACTASes
dc.titleIntuitionistic Hypothetical Logic of Proofes
dc.typeinfo:eu-repo/semantics/article
dc.typeinfo:ar-repo/semantics/artículo
dc.typeinfo:eu-repo/semantics/publishedVersion

Archivos

Bloque original

Miniatura
Nombre:
CONICET_Digital_Nro.abe754e1-f508-4e2a-9c5c-4edcda1da11c_A.pdf
Tamaño:
301.98 KB
Formato:
Adobe Portable Document Format
Descargar

Colecciones

Articulos(SEDE CENTRAL)
Volver a la Vista simple