{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T18:28:19Z","timestamp":1693852099215},"reference-count":0,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2003,5,20]],"date-time":"2003-05-20T00:00:00Z","timestamp":1053388800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2003,6]]},"abstract":"<jats:p>We refine the simulation technique introduced in Di Cosmo and Kesner (1997) to show strong \nnormalisation of <jats:inline-formula id=\"ffm002\">$\\l$<\/jats:inline-formula>-calculi with explicit substitutions <jats:italic>via<\/jats:italic> termination of cut elimination in proof nets (Girard 1987). We first propose a notion of equivalence relation for proof nets that extends the one in Di Cosmo and Guerrini (1999), and show that cut elimination modulo this equivalence relation is terminating. We then show strong normalisation of the typed version of the <jats:inline-formula id=\"ffm003\">$\\ll$<\/jats:inline-formula>-calculus with de Bruijn indices (a calculus with full composition defined in David and Guillaume (1999)) using a translation from typed <jats:inline-formula id=\"ffm004\">$\\ll$<\/jats:inline-formula> to proof nets. Finally, we propose a version of typed <jats:inline-formula id=\"ffm005\">$\\ll$<\/jats:inline-formula> with named variables, which helps to give a better understanding of the complex mechanism of the explicit weakening notation introduced in the <jats:inline-formula id=\"ffm006\">$\\ll$<\/jats:inline-formula>-calculus with de Bruijn indices (David and Guillaume 1999).<\/jats:p>","DOI":"10.1017\/s0960129502003791","type":"journal-article","created":{"date-parts":[[2003,5,22]],"date-time":"2003-05-22T05:12:38Z","timestamp":1053580358000},"page":"409-450","source":"Crossref","is-referenced-by-count":18,"title":["Proof nets and explicit substitutions"],"prefix":"10.1017","volume":"13","author":[{"given":"ROBERTO","family":"DI COSMO","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"DELIA","family":"KESNER","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"EMMANUEL","family":"POLONOVSKI","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2003,5,20]]},"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129502003791","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,30]],"date-time":"2019-03-30T15:06:58Z","timestamp":1553958418000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129502003791\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5,20]]},"references-count":0,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,6]]}},"alternative-id":["S0960129502003791"],"URL":"https:\/\/doi.org\/10.1017\/s0960129502003791","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,5,20]]}}}