DC FieldValueLanguage
dc.contributor.authorBarendregt, Henken_US
dc.contributor.authorGhilezan, Silviaen_US
dc.date.accessioned2020-05-02T16:42:23Z-
dc.date.available2020-05-02T16:42:23Z-
dc.date.issued2000-01-01-
dc.identifier.issn0956-7968en
dc.identifier.urihttp://researchrepository.mi.sanu.ac.rs/handle/123456789/2615-
dc.description.abstractIt is well known that there is an isomorphism between natural deduction derivations and typed lambda terms. Moreover, normalising these terms corresponds to eliminating cuts in the equivalent sequent calculus derivations. Several papers have been written on this topic. The correspondence between sequent calculus derivations and natural deduction derivations is, however, not a one-one map, which causes some syntactic technicalities. The correspondence is best explained by two extensionally equivalent type assignment systems for untyped lambda terms, one corresponding to natural deduction (λN) and the other to sequent calculus (λL). These two systems constitute different grammars for generating the same (type assignment relation for untyped) lambda terms. The second grammar is ambiguous, but the first one is not. This fact explains the many-one correspondence mentioned above. Moreover, the second type assignment system has a 'cut-free' fragment (λLcf). This fragment generates exactly the typeable lambda terms in normal form. The cut elimination theorem becomes a simple consequence of the fact that typed lambda terms posses a normal form.en_US
dc.publisherCambridge University Press-
dc.relation.ispartofJournal of Functional Programmingen_US
dc.titleLambda terms for natural deduction, sequent calculus and cut eliminationen_US
dc.typeArticleen_US
dc.identifier.doi10.1017/S0956796899003524-
dc.identifier.scopus2-s2.0-0347268436-
dc.relation.firstpage121en
dc.relation.lastpage134en
dc.relation.issue1en
dc.relation.volume10en
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.openairetypeArticle-
item.cerifentitytypePublications-
item.grantfulltextnone-
item.fulltextNo Fulltext-
crisitem.author.orcid0000-0003-2253-8285-
Show simple item record

SCOPUSTM   
Citations

23
checked on Jan 31, 2023

Page view(s)

27
checked on Jan 31, 2023

Google ScholarTM

Check

Altmetric

Altmetric


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