DC FieldValueLanguage
dc.contributor.authorDougherty, Danielen
dc.contributor.authorGhilezan, Silviaen
dc.contributor.authorLescanne, Pierreen
dc.date.accessioned2020-05-02T16:42:21Z-
dc.date.available2020-05-02T16:42:21Z-
dc.date.issued2008-05-28en
dc.identifier.issn0304-3975en
dc.description.abstractWe develop an intersection type system for the over(λ, -) μ over(μ, ̃) calculus of Curien and Herbelin. This calculus provides a symmetric computational interpretation of classical sequent style logic and gives a simple account of call-by-name and call-by-value. The present system improves upon earlier type disciplines for over(λ, -) μ over(μ, ̃): in addition to characterizing the over(λ, -) μ over(μ, ̃) expressions that are strongly normalizing under free (unrestricted) reduction, the system enjoys the Subject Reduction and the Subject Expansion properties.en
dc.publisherElsevier-
dc.relation.ispartofTheoretical Computer Scienceen
dc.subjectClassical logic | Intersection-types | Sequent calculusen
dc.titleCharacterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: Extending the Coppo-Dezani heritageen
dc.typeArticleen
dc.identifier.doi10.1016/j.tcs.2008.01.022en
dc.identifier.scopus2-s2.0-43049098185en
dc.relation.firstpage114en
dc.relation.lastpage128en
dc.relation.issue1-3en
dc.relation.volume398en
dc.description.rankM22-
item.fulltextNo Fulltext-
item.openairetypeArticle-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.cerifentitytypePublications-
item.grantfulltextnone-
crisitem.author.orcid0000-0003-2253-8285-
Show simple item record

SCOPUSTM   
Citations

15
checked on Nov 27, 2022

Page view(s)

19
checked on Nov 28, 2022

Google ScholarTM

Check

Altmetric

Altmetric


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