{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,10]],"date-time":"2026-10-10T02:06:54Z","timestamp":1791598014121,"version":"4.3.4"},"reference-count":27,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,12,5]],"date-time":"2014-12-05T00:00:00Z","timestamp":1417737600000},"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":[[2016,1]]},"abstract":"<jats:p>We give an algebraic characterization of the syntax and semantics of a class of untyped functional programming languages.<\/jats:p><jats:p>To this end, we introduce a notion of 2-<jats:italic>signature<\/jats:italic>: such a signature specifies not only the <jats:italic>terms<\/jats:italic> of a language, but also <jats:italic>reduction rules<\/jats:italic> on those terms. To any 2-signature (<jats:italic>S, A<\/jats:italic>) we associate a category of \u2018models\u2019. We then prove that this category has an initial object, which integrates the terms freely generated by <jats:italic>S<\/jats:italic>, and which is equipped with reductions according to the rules given in <jats:italic>A<\/jats:italic>. We call this initial object the <jats:italic>programming language generated by<\/jats:italic> (<jats:italic>S, A<\/jats:italic>). Models of a 2-signature are built from <jats:italic>relative monads<\/jats:italic> and <jats:italic>modules<\/jats:italic> over such monads. Through the use of monads, the models \u2013 and in particular, the initial model \u2013 come equipped with a <jats:italic>substitution operation<\/jats:italic> that is compatible with reduction in a suitable sense.<\/jats:p><jats:p>The initiality theorem is formalized in the proof assistant Coq, yielding a machinery which, when fed with a 2-signature, provides the associated programming language with reduction relation and certified substitution.<\/jats:p>","DOI":"10.1017\/s0960129514000103","type":"journal-article","created":{"date-parts":[[2014,12,5]],"date-time":"2014-12-05T04:58:59Z","timestamp":1417755539000},"page":"3-37","source":"Crossref","is-referenced-by-count":8,"title":["Modules over relative monads for syntax and semantics"],"prefix":"10.1017","volume":"26","author":[{"given":"BENEDIKT","family":"AHRENS","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,12,5]]},"reference":[{"key":"S0960129514000103_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054285"},{"key":"S0960129514000103_ref22","volume-title":"Categories for the Working Mathematician","author":"Mac Lane","year":"1998"},{"key":"S0960129514000103_ref20","first-page":"204","volume-title":"14th Annual Symposium on Logic in Computer Science","author":"Hofmann","year":"1999"},{"key":"S0960129514000103_ref27","unstructured":"Zsid\u00f3 J. (2010) Typed abstract syntax. Available at http:\/\/tel.archives-ouvertes.fr\/tel-00535944\/. Ph.D. thesis, University of Nice, France."},{"key":"S0960129514000103_ref7","unstructured":"Coq (2010) The coq proof assistant. Available at: http:\/\/coq.inria.fr. URL: http:\/\/coq.inria.fr."},{"key":"S0960129514000103_ref12","doi-asserted-by":"crossref","unstructured":"Fiore M. et al. (1999) Abstract syntax and variable binding. In: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science. LICS '99, Washington, DC, USA: IEEE Computer Society 193\u2013202. ISBN: 0-7695-0158-3.","DOI":"10.1109\/LICS.1999.782615"},{"key":"S0960129514000103_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.024"},{"key":"S0960129514000103_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73445-1_16"},{"key":"S0960129514000103_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12032-9_21"},{"key":"S0960129514000103_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/1088454.1088457"},{"key":"S0960129514000103_ref19","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(3:10)2013"},{"key":"S0960129514000103_ref23","first-page":"184","volume-title":"Principles and Practice of Declarative Programming","author":"Miculan","year":"2003"},{"key":"S0960129514000103_ref13","doi-asserted-by":"crossref","unstructured":"Gabbay M. and Pitts A. (1999) A new approach to abstract syntax involving binders. In: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science. LICS '99, Washington, DC, USA: IEEE Computer Society 214\u2013224. ISBN: 0-7695-0158-3.","DOI":"10.1109\/LICS.1999.782617"},{"key":"S0960129514000103_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.12.002"},{"key":"S0960129514000103_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"S0960129514000103_ref3","doi-asserted-by":"crossref","unstructured":"Altenkirch T. and Reus B. (1999) Monadic presentations of lambda terms using generalized inductive types. In: Computer Science Logic, 13th International Workshop, CSL '99 453\u2013468.","DOI":"10.1007\/3-540-48168-0_32"},{"key":"S0960129514000103_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31982-5_2"},{"key":"S0960129514000103_ref21","unstructured":"Hur C.-K. (2010) Categorical Equational Systems: Algebraic Models and Equational Reasoning, Ph.D. thesis, University of Cambridge, UK."},{"key":"S0960129514000103_ref5","unstructured":"Barendregt H. and Barendsen E. (1994) Introduction to lambda calculus. Available at: ftp:\/\/ftp.cs.ru.nl\/pub\/CompMath.Found\/lambda.pdf. revised 2000."},{"key":"S0960129514000103_ref2","first-page":"25","article-title":"Initial semantics for higher\u2013order typed syntax in Coq","volume":"4.1","author":"Ahrens","year":"2011","journal-title":"Journal of Formalized Reasoning"},{"key":"S0960129514000103_ref1","first-page":"1","article-title":"Extended initiality for typed abstract syntax","volume":"8.2","author":"Ahrens","year":"2012","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129514000103_ref14","first-page":"341","article-title":"A new approach to abstract syntax with variable binding","volume":"13.3\u20135","author":"Gabbay","year":"2001","journal-title":"Formal Aspects of Computing"},{"key":"S0960129514000103_ref15","first-page":"290","article-title":"Rewriting via coinserters","volume":"10.4","author":"Ghani","year":"2003","journal-title":"Nordic Journal of Computing"},{"key":"S0960129514000103_ref17","unstructured":"Hirschowitz A. and Maggesi M. (2007b) The algebraicity of the lambda-calculus. In: CoRR abs\/0704.2900. Available at http:\/\/arxiv.org\/abs\/0704.2900."},{"key":"S0960129514000103_ref9","doi-asserted-by":"crossref","unstructured":"Fiore M. (2002) Semantic analysis of normalisation by evaluation for typed lambda calculus. In: Proceedings of the 4th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming. PPDP'02, Pittsburgh, PA, USA: ACM 26\u201337. ISBN: 1-58113-528-9. doi: http:\/\/doi.acm.org\/10.1145\/571157.571161.","DOI":"10.1145\/571157.571161"},{"key":"S0960129514000103_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.07.003"},{"key":"S0960129514000103_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73420-8_53"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000103","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T19:48:08Z","timestamp":1555703288000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000103\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12,5]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,1]]}},"alternative-id":["S0960129514000103"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000103","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,12,5]]}}}