{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:35Z","timestamp":1753889795584,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2017,9,28]],"date-time":"2017-09-28T00:00:00Z","timestamp":1506556800000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"},{"start":{"date-parts":[[2017,9,28]],"date-time":"2017-09-28T00:00:00Z","timestamp":1506556800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"},{"start":{"date-parts":[[2017,9,28]],"date-time":"2017-09-28T00:00:00Z","timestamp":1506556800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"accepted":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p>In this paper we give an arithmetical proof of the strong normalization of lambda-Sym-Prop of Berardi and Barbanera [1], which can be considered as a formulae-as-types translation of classical propositional logic in natural deduction style. Then we give a translation between the lambda-Sym-Prop-calculus and the lambda-bar-mu-mu-tilde-star-calculus, which is the implicational part of the lambda-bar-mu-mu-tilde-calculus invented by Curien and Herbelin [3] extended with negation. In this paper we adapt the method of David and Nour [4] for proving strong normalization. The novelty in our proof is the notion of zoom-in sequences of redexes, which leads us directly to the proof of the main theorem.<\/jats:p>","DOI":"10.23638\/lmcs-13(3:34)2017","type":"journal-article","created":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T17:34:41Z","timestamp":1743701681000},"source":"Crossref","is-referenced-by-count":0,"title":["Strong normalization of lambda-Sym-Prop- and lambda-bar-mu-mu-tilde-star- calculi"],"prefix":"10.23638","volume":"Volume 13, Issue 3","author":[{"given":"Peter","family":"Battyanyi","sequence":"first","affiliation":[]},{"given":"Karim","family":"Nour","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2017,9,28]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/arxiv.org\/pdf\/1706.07246v2","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/arxiv.org\/pdf\/1706.07246v2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T17:34:41Z","timestamp":1743701681000},"score":1,"resource":{"primary":{"URL":"http:\/\/lmcs.episciences.org\/3963"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,28]]},"references-count":0,"URL":"https:\/\/doi.org\/10.23638\/lmcs-13(3:34)2017","relation":{"is-same-as":[{"id-type":"arxiv","id":"1706.07246","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1706.07246","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2017,9,28]]},"article-number":"3963"}}