{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:54:40Z","timestamp":1776891280995,"version":"3.51.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","issue":"1","license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2000,1]]},"abstract":"<jats:p>\n                    It is well known that there is an isomorphism between natural deduction derivations and \ntyped lambda terms. Moreover, normalising these terms corresponds to eliminating cuts in the \nequivalent sequent calculus derivations. Several papers have been written on this topic. The \ncorrespondence between sequent calculus derivations and natural deduction derivations is, \nhowever, not a one-one map, which causes some syntactic technicalities. The correspondence \nis best explained by two extensionally equivalent type assignment systems for untyped lambda \nterms, one corresponding to natural deduction (\u03bb\n                    <jats:italic>N<\/jats:italic>\n                    ) \nand the other to sequent calculus (\u03bb\n                    <jats:italic>L<\/jats:italic>\n                    ). \nThese two systems constitute different grammars for generating the same (type assignment \nrelation for untyped) lambda terms. The second grammar is ambiguous, but the first one is \nnot. This fact explains the many-one correspondence mentioned above. Moreover, the second \ntype assignment system has a \u2018cut-free\u2019 fragment \n(\u03bb\n                    <jats:italic>L<\/jats:italic>\n                    <jats:sup>cf<\/jats:sup>\n                    ). This fragment generates exactly \nthe typeable lambda terms in normal form. The cut elimination theorem becomes a simple \nconsequence of the fact that typed lambda terms possess a normal form.\n                  <\/jats:p>","DOI":"10.1017\/s0956796899003524","type":"journal-article","created":{"date-parts":[[2002,7,27]],"date-time":"2002-07-27T09:26:15Z","timestamp":1027761975000},"page":"121-134","source":"Crossref","is-referenced-by-count":19,"title":["Lambda terms for natural deduction, \nsequent calculus and cut elimination"],"prefix":"10.46298","volume":"10","author":[{"given":"HENK","family":"BARENDREGT","sequence":"first","affiliation":[]},{"given":"SILVIA","family":"GHILEZAN","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2000,1,1]]},"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796899003524","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:18:32Z","timestamp":1776889112000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796899003524\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,1]]},"references-count":0,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2000,1]]}},"alternative-id":["S0956796899003524"],"URL":"https:\/\/doi.org\/10.1017\/s0956796899003524","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000,1]]}}}