{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,23]],"date-time":"2026-04-23T09:02:12Z","timestamp":1776934932758,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642198045","type":"print"},{"value":"9783642198052","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-19805-2_26","type":"book-chapter","created":{"date-parts":[[2011,3,14]],"date-time":"2011-03-14T13:05:14Z","timestamp":1300107914000},"page":"381-395","source":"Crossref","is-referenced-by-count":11,"title":["Polymorphic Abstract Syntax via Grothendieck Construction"],"prefix":"10.1007","author":[{"given":"Makoto","family":"Hamana","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","unstructured":"Aczel, P.: A general Church-Rosser theorem. Technical report, University of Manchester (1978)"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., Hofmann, M., Streicher, T.: Reduction-free normalisation for a polymorphic system. In: Proc. of LICS 1996, pp. 98\u2013106 (1996)","DOI":"10.1109\/LICS.1996.561309"},{"key":"26_CR3","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. Bruijn de","year":"1972","unstructured":"de Bruijn, N.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae\u00a034, 381\u2013391 (1972)","journal-title":"Indagationes Mathematicae"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-642-15205-4_26","volume-title":"Computer Science Logic","author":"M. Fiore","year":"2010","unstructured":"Fiore, M., Hur, C.-K.: Second-order equational logic. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol.\u00a06247, pp. 320\u2013335. Springer, Heidelberg (2010)"},{"key":"26_CR5","first-page":"26","volume-title":"Proc. of PPDP 2002","author":"M. Fiore","year":"2002","unstructured":"Fiore, M.: Semantic analysis of normalisation by evaluation for typed lambda calculus. In: Proc. of PPDP 2002, pp. 26\u201337. ACM Press, New York (2002)"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Fiore, M.: Second-order and dependently-sorted abstract syntax. In: Proc. of LICS 2008, pp. 57\u201368 (2008)","DOI":"10.1109\/LICS.2008.38"},{"key":"26_CR7","unstructured":"Fiore, M.: Algebraic meta-theories and synthesis of equational logics (2009), Research Programme"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proc. of LICS 1999, pp. 193\u2013202 (1999)","DOI":"10.1109\/LICS.1999.782615"},{"key":"26_CR9","series-title":"Lecture Notes in Mathematics","first-page":"145","volume-title":"Rev\u00eatement Etales et Groupe Fondamental (SGA1)","author":"A. Grothendieck","year":"1970","unstructured":"Grothendieck, A.: Cat\u00e9gories fibr\u00e9es et descente (expos\u00e9 VI). In: Grothendieck, A. (ed.) Rev\u00eatement Etales et Groupe Fondamental (SGA1). Lecture Notes in Mathematics, vol.\u00a0224, pp. 145\u2013194. Springer, Heidelberg (1970)"},{"key":"26_CR10","unstructured":"Goguen, J., Thatcher, J., Wagner, E.: An initial algebra approach to the specification, correctness and implementation of abstract data types. Technical Report RC 6487, IBM T. J. Watson Research Center (1976)"},{"issue":"2\/3","key":"26_CR11","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10990-006-8748-4","volume":"19","author":"N. Ghani","year":"2006","unstructured":"Ghani, N., Uustalu, T., Hamana, M.: Explicit substitutions and higher-order syntax. Higher-Order and Symbolic Computation\u00a019(2\/3), 263\u2013282 (2006)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-540-30477-7_23","volume-title":"Programming Languages and Systems","author":"M. Hamana","year":"2004","unstructured":"Hamana, M.: Free \u03a3-monoids: A higher-order syntax with metavariables. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol.\u00a03302, pp. 348\u2013363. Springer, Heidelberg (2004)"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-32033-3_11","volume-title":"Term Rewriting and Applications","author":"M. Hamana","year":"2005","unstructured":"Hamana, M.: Universal algebra for termination of higher-order rewriting. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 135\u2013149. Springer, Heidelberg (2005)"},{"key":"26_CR14","first-page":"97","volume-title":"Proc. of PPDP 2007","author":"M. Hamana","year":"2007","unstructured":"Hamana, M.: Higher-order semantic labelling for inductive datatype systems. In: Proc. of PPDP 2007, pp. 97\u2013108. ACM Press, New York (2007)"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Hamana, M.: Initial algebra semantics for cyclic sharing tree structures. Logical Methods in Computer Science\u00a06(3) (2010)","DOI":"10.2168\/LMCS-6(3:15)2010"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: Semantical analysis of higher-order abstract syntax. In: Proc. of LICS 1999, pp. 204\u2013213 (1999)","DOI":"10.1109\/LICS.1999.782616"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"831","DOI":"10.1007\/978-3-540-27836-8_70","volume-title":"Automata, Languages and Programming","author":"S. Katsumata","year":"2004","unstructured":"Katsumata, S.: A generalisation of pre-logical predicates to simply typed formal systems. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol.\u00a03142, pp. 831\u2013845. Springer, Heidelberg (2004)"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Morris, P., Altenkirch, T.: Indexed containers. In: LICS 2009, pp. 277\u2013285 (2009)","DOI":"10.1109\/LICS.2009.33"},{"key":"26_CR19","series-title":"ENTCS","first-page":"275","volume-title":"Proc. of MFPS XXIV","author":"M. Miculan","year":"2008","unstructured":"Miculan, M.: A categorical model of the Fusion calculus. In: Proc. of MFPS XXIV. ENTCS, vol.\u00a0218, pp. 275\u2013293. Elsevier, Amsterdam (2008)"},{"key":"26_CR20","first-page":"184","volume-title":"Proc. of PPDP 2003","author":"M. Miculan","year":"2003","unstructured":"Miculan, M., Scagnetto, I.: A framework for typed HOAS and semantics. In: Proc. of PPDP 2003, pp. 184\u2013194. ACM Press, New York (2003)"},{"issue":"4","key":"26_CR21","doi-asserted-by":"publisher","first-page":"763","DOI":"10.1137\/0211062","volume":"11","author":"M.B. Smyth","year":"1982","unstructured":"Smyth, M.B., Plotkin, G.D.: The category-theoretic solution of recursive domain equations. SIAM J. Comput\u00a011(4), 763\u2013783 (1982)","journal-title":"SIAM J. Comput"},{"issue":"2","key":"26_CR22","first-page":"221","volume":"84","author":"M. Tanaka","year":"2008","unstructured":"Tanaka, M., Power, J.: Category theoretic semantics for typed binding signatures with recursion. Fundam. Inform.\u00a084(2), 221\u2013240 (2008)","journal-title":"Fundam. Inform."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19805-2_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,4]],"date-time":"2025-03-04T07:09:20Z","timestamp":1741072160000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19805-2_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642198045","9783642198052"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19805-2_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}