{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:58Z","timestamp":1753889818309,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2013,2,27]],"date-time":"2013-02-27T00:00:00Z","timestamp":1361923200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"name":"National Science Foundation","award":["0910510"],"award-info":[{"award-number":["0910510"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>This paper shows how a recently developed view of typing as small-step\nabstract reduction, due to Kuan, MacQueen, and Findler, can be used to recast\nthe development of simple type theory from a rewriting perspective. We show how\nstandard meta-theoretic results can be proved in a completely new way, using\nthe rewriting view of simple typing. These meta-theoretic results include\nstandard type preservation and progress properties for simply typed lambda\ncalculus, as well as generalized versions where typing is taken to include both\nabstract and concrete reduction. We show how automated analysis tools developed\nin the term-rewriting community can be used to help automate the proofs for\nthis meta-theory. Finally, we show how to adapt a standard proof of\nnormalization of simply typed lambda calculus, for the rewriting approach to\ntyping.<\/jats:p>","DOI":"10.2168\/lmcs-9(1:4)2013","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T13:36:16Z","timestamp":1385732176000},"source":"Crossref","is-referenced-by-count":2,"title":["A Rewriting View of Simple Typing"],"prefix":"10.46298","volume":"Volume 9, Issue 1","author":[{"given":"Aaron","family":"Stump","sequence":"first","affiliation":[]},{"given":"Garrin","family":"Kimmell","sequence":"additional","affiliation":[]},{"given":"Hans","family":"Zantema","sequence":"additional","affiliation":[]},{"given":"Ruba El Haj","family":"Omar","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2013,2,27]]},"reference":[{"key":"696:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/936\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/936\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:59:29Z","timestamp":1681243169000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/936"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,2,27]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-9(1:4)2013","relation":{"is-same-as":[{"id-type":"arxiv","id":"1211.0865","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1211.0865","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2013,2,27]]},"article-number":"936"}}