DC FieldValueLanguage
dc.contributor.authorGhilezan, Silviaen
dc.contributor.authorLescanne, Pierreen
dc.date.accessioned2020-05-02T16:42:22Z-
dc.date.available2020-05-02T16:42:22Z-
dc.date.issued2004-12-01en
dc.identifier.isbn978-3-540-22164-7-
dc.identifier.issn0302-9743en
dc.description.abstractCurien and Herbelin provided a Curry and Howard correspondence between classical prepositional logic and a computational model called λ̄μμμ which is a calculus for interpreting classical sequents. A new terminology for λ̄μμ̄ in terms of pairs of callers-callees which we name capsules enlightens a natural link between λ̄μμ̄ and process calculi. In this paper we propose an intersection type system λ̄μμ̄ which is an extension of λ̄μμ̄ with intersection types. We prove that all strongly normalizing λ̄μμ̄-terms are typeable in the new system, which was not the case in λ̄μμ̃. Also, we prove that all typeable μ̃-free terms are strongly normalizing.en
dc.publisherSpringer Link-
dc.relation.ispartofLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)en
dc.titleClassical Proofs, Typed Processes, and Intersection Types Extended Abstracten
dc.typeArticleen
dc.relation.conferenceInternational Workshop on Types for Proofs and Programs, TYPES 2003-
dc.identifier.doi10.1007/978-3-540-24849-1_15-
dc.identifier.scopus2-s2.0-35048848953en
dc.relation.firstpage226en
dc.relation.lastpage241en
dc.relation.volume3085en
dc.description.rankM22-
item.openairetypeArticle-
item.fulltextNo Fulltext-
item.grantfulltextnone-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.cerifentitytypePublications-
crisitem.author.orcid0000-0003-2253-8285-
Show simple item record

SCOPUSTM   
Citations

1
checked on Nov 27, 2022

Page view(s)

23
checked on Nov 28, 2022

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.