{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:28:33Z","timestamp":1754483313011,"version":"3.41.2"},"reference-count":24,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,4,6]],"date-time":"2012-04-06T00:00:00Z","timestamp":1333670400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Initial Semantics aims at interpreting the syntax associated to a signature\nas the initial object of some category of 'models', yielding induction and\nrecursion principles for abstract syntax. Zsid\\'o proves an initiality result\nfor simply-typed syntax: given a signature S, the abstract syntax associated to\nS constitutes the initial object in a category of models of S in monads.\nHowever, the iteration principle her theorem provides only accounts for\ntranslations between two languages over a fixed set of object types. We\ngeneralize Zsid\\'o's notion of model such that object types may vary, yielding\na larger category, while preserving initiality of the syntax therein. Thus we\nobtain an extended initiality theorem for typed abstract syntax, in which\ntranslations between terms over different types can be specified via the\nassociated category-theoretic iteration operator as an initial morphism. Our\ndefinitions ensure that translations specified via initiality are type-safe,\ni.e. compatible with the typing in the source and target language in the\nobvious sense. Our main example is given via the propositions-as-types\nparadigm: we specify propositions and inference rules of classical and\nintuitionistic propositional logics through their respective typed signatures.\nAfterwards we use the category--theoretic iteration operator to specify a\ndouble negation translation from the former to the latter. A second example is\ngiven by the signature of PCF. For this particular case, we formalize the\ntheorem in the proof assistant Coq. Afterwards we specify, via the\ncategory-theoretic iteration operator, translations from PCF to the untyped\nlambda calculus.<\/jats:p>","DOI":"10.2168\/lmcs-8(2:1)2012","type":"journal-article","created":{"date-parts":[[2013,9,23]],"date-time":"2013-09-23T14:50:43Z","timestamp":1379947843000},"source":"Crossref","is-referenced-by-count":3,"title":["Extended Initiality for Typed Abstract Syntax"],"prefix":"10.46298","volume":"Volume 8, Issue 2","author":[{"given":"Benedikt","family":"Ahrens","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,4,6]]},"reference":[{"key":"10.2168\/LMCS-8(2:1)2012_DBLP:conf\/fossacs\/AltenkirchCU10","doi-asserted-by":"crossref","unstructured":"Thorsten Altenkirch, James Chapman, and Tarmo Uustalu. Monads Need Not Be Endofunctors. In C.-H. Luke Ong, editor,FOSSACS, volume 6014 ofLecture Notes in Computer Science, pages 297-311. Springer, 2010.","DOI":"10.1007\/978-3-642-12032-9_21"},{"key":"10.2168\/LMCS-8(2:1)2012_ahrens_relmonads","unstructured":"Benedikt Ahrens. Modules over relative monads for syntax and semantics. 2011. To be published in Math. Struct. in Comp. Science, http:\/\/arxiv.org\/abs\/1107.5252."},{"key":"10.2168\/LMCS-8(2:1)2012_alt_reus","doi-asserted-by":"crossref","unstructured":"Thorsten Altenkirch and Bernhard Reus. Monadic presentations of lambda terms using generalized inductive types. InComputer Science Logic, 13th International Workshop, CSL '99, pages 453-468, 1999.","DOI":"10.1007\/3-540-48168-0_32"},{"issue":"1","key":"10.2168\/LMCS-8(2:1)2012_ahrens_zsido","first-page":"25","volume":"4","author":"Benedikt Ahrens and Julianna Zsid\u00f3","year":"2011","journal-title":"Journal of Formalized Reasoning"},{"key":"10.2168\/LMCS-8(2:1)2012_dep_syn","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"10.2168\/LMCS-8(2:1)2012_birkhoff1935","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100013463"},{"key":"10.2168\/LMCS-8(2:1)2012_BirdMeertens98:Nested","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054285"},{"key":"10.2168\/LMCS-8(2:1)2012_coq","unstructured":"Coq. The Coq Proof Assistant. http:\/\/coq.inria.fr, 2010."},{"key":"10.2168\/LMCS-8(2:1)2012_DBLP:conf\/icalp\/FioreH07","doi-asserted-by":"crossref","unstructured":"Marcelo P. Fiore and Chung-Kil Hur. Equational systems and free constructions (extended abstract). In Lars Arge, Christian Cachin, Tomasz Jurdzinski, and Andrzej Tarlecki, editors,ICALP, volume 4596 ofLecture Notes in Computer Science, pages 607-618. Springer, 2007.","DOI":"10.1007\/978-3-540-73420-8_53"},{"key":"10.2168\/LMCS-8(2:1)2012_fio02","doi-asserted-by":"crossref","unstructured":"Marcelo Fiore. Semantic analysis of normalisation by evaluation for typed lambda calculus. InProceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, PPDP '02, pages 26-37, New York, NY, USA, 2002. ACM.","DOI":"10.1145\/571157.571161"},{"key":"10.2168\/LMCS-8(2:1)2012_fpt","unstructured":"Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax and variable binding. InProceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, LICS '99, pages 193-202, Washington, DC, USA, 1999. IEEE Computer Society."},{"key":"10.2168\/LMCS-8(2:1)2012_gabbay_pitts99","unstructured":"Murdoch J. Gabbay and Andrew M. Pitts. A New Approach to Abstract Syntax Involving Binders. In14th Annual Symposium on Logic in Computer Science, pages 214-224, Washington, DC, USA, 1999. IEEE Computer Society Press."},{"key":"10.2168\/LMCS-8(2:1)2012_gtww","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321997"},{"key":"10.2168\/LMCS-8(2:1)2012_DBLP:conf\/wollic\/HirschowitzM07","doi-asserted-by":"crossref","unstructured":"Andr\u00e9 Hirschowitz and Marco Maggesi. Modules over monads and linearity. In Daniel Leivant and Ruy J. G. B. de Queiroz, editors,WoLLIC, volume 4576 ofLecture Notes in Computer Science, pages 218-237. Springer, 2007.","DOI":"10.1007\/978-3-540-73445-1_16"},{"issue":"5","key":"10.2168\/LMCS-8(2:1)2012_DBLP:journals\/iandc\/HirschowitzM10","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1016\/j.ic.2009.07.003","volume":"208","author":"Andr\u00e9 Hirschowitz and Marco Maggesi","year":"2010","journal-title":"Inf. Comput."},{"key":"10.2168\/LMCS-8(2:1)2012_Hyland00onfull","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1006\/inco.2000.2917","volume":"163","author":"J. M. E. Hyland and C.-H. Ong","year":"2000","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-8(2:1)2012_hofmann","unstructured":"Martin Hofmann. Semantical Analysis of Higher-Order Syntax. InIn 14th Annual Symposium on Logic in Computer Science, pages 204-213. IEEE Computer Society Press, 1999."},{"key":"10.2168\/LMCS-8(2:1)2012_hur_phd","unstructured":"Chung-Kil Hur.Categorical equational systems: algebraic models and equational reasoning. PhD thesis, University of Cambridge, UK, 2010."},{"key":"10.2168\/LMCS-8(2:1)2012_Leinster_2004","doi-asserted-by":"crossref","unstructured":"Tom Leinster.Higher operads, higher categories, volume 298 ofLondon Mathematical Society Lecture Note Series. Cambridge University Press, 2004. http:\/\/arxiv.org\/abs\/math\/0305049.","DOI":"10.1017\/CBO9780511525896"},{"key":"10.2168\/LMCS-8(2:1)2012_manes","doi-asserted-by":"crossref","unstructured":"Ernest Manes.Algebraic Theories, volume 26 ofGraduate Texts in Mathematics. Springer, 1976.","DOI":"10.1007\/978-1-4612-9860-1"},{"key":"10.2168\/LMCS-8(2:1)2012_DBLP:conf\/ppdp\/MiculanS03","doi-asserted-by":"crossref","unstructured":"Marino Miculan and Ivan Scagnetto. A framework for typed HOAS and semantics. InPPDP, pages 184-194. ACM, 2003.","DOI":"10.1145\/888251.888269"},{"issue":"3","key":"10.2168\/LMCS-8(2:1)2012_Plotkin1977223","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"Gordon D. Plotkin","year":"1977","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(2:1)2012_TVD88","unstructured":"A. S. Troelstra and D. van Dalen.Constructivism in Mathematics: an Introduction, volume I and II. North-Holland, Amsterdam, 1988."},{"key":"10.2168\/LMCS-8(2:1)2012_ju_phd","unstructured":"Julianna Zsid\u00f3.Typed Abstract Syntax. PhD thesis, University of Nice, France, 2010. http:\/\/tel.archives-ouvertes.fr\/tel-00535944\/."}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1193\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1193\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:05:41Z","timestamp":1681243541000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1193"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,4,6]]},"references-count":24,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(2:1)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1107.4751","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1107.4751","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,4,6]]},"article-number":"1193"}}