{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:35:47Z","timestamp":1753889747931,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2007,12,4]],"date-time":"2007-12-04T00:00:00Z","timestamp":1196726400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Ulrich Berger presented a powerful proof of strong normalisation using\ndomains, in particular it simplifies significantly Tait's proof of strong\nnormalisation of Spector's bar recursion. The main contribution of this paper\nis to show that, using ideas from intersection types and Martin-Lof's domain\ninterpretation of type theory one can in turn simplify further U. Berger's\nargument. We build a domain model for an untyped programming language where U.\nBerger has an interpretation only for typed terms or alternatively has an\ninterpretation for untyped terms but need an extra condition to deduce strong\nnormalisation. As a main application, we show that Martin-L\\\"{o}f dependent\ntype theory extended with a program for Spector double negation shift.<\/jats:p>","DOI":"10.2168\/lmcs-3(4:12)2007","type":"journal-article","created":{"date-parts":[[2008,6,3]],"date-time":"2008-06-03T13:15:14Z","timestamp":1212498914000},"source":"Crossref","is-referenced-by-count":6,"title":["A proof of strong normalisation using domain theory"],"prefix":"10.46298","volume":"Volume 3, Issue 4","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]},{"given":"Arnaud","family":"Spiwack","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2007,12,4]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1099\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1099\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:03:27Z","timestamp":1681243407000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1099"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,12,4]]},"references-count":0,"URL":"https:\/\/doi.org\/10.2168\/lmcs-3(4:12)2007","relation":{"is-same-as":[{"id-type":"arxiv","id":"0709.1401","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.0709.1401","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2007,12,4]]},"article-number":"1099"}}