{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:14:27Z","timestamp":1770290067288,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642152047","type":"print"},{"value":"9783642152054","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15205-4_26","type":"book-chapter","created":{"date-parts":[[2010,8,13]],"date-time":"2010-08-13T14:48:24Z","timestamp":1281710904000},"page":"320-335","source":"Crossref","is-referenced-by-count":21,"title":["Second-Order Equational Logic (Extended Abstract)"],"prefix":"10.1007","author":[{"given":"Marcelo","family":"Fiore","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chung-Kil","family":"Hur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","unstructured":"Aczel, P.: A general Church-Rosser theorem. Typescript (1978)"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Aczel, P.: Frege structures and the notion of proposition, truth and set. In: The Kleene Symposium, pp. 31\u201359 (1980)","DOI":"10.1016\/S0049-237X(08)71252-7"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. CUP (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"26_CR4","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1017\/S0305004100013463","volume":"31","author":"G. Birkhoff","year":"1935","unstructured":"Birkhoff, G.: On the structure of abstract algebras. P. Camb. Philos. Soc.\u00a031, 433\u2013454 (1935)","journal-title":"P. Camb. Philos. Soc."},{"key":"26_CR5","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"J. Symbolic Logic"},{"key":"26_CR6","first-page":"223","volume":"172","author":"R. Clouston","year":"2007","unstructured":"Clouston, R., Pitts, A.: Nominal equational logic. ENTCS\u00a0172, 223\u2013257 (2007)","journal-title":"ENTCS"},{"key":"26_CR7","unstructured":"Fiore, M.: Algebraic meta-theories and synthesis of equational logics. Research Programme (2009)"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Fiore, M.: Semantic analysis of normalisation by evaluation for typed lambda calculus. In: PPDP 2002, pp. 26\u201337 (2002)","DOI":"10.1145\/571157.571161"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/978-3-540-31982-5_2","volume-title":"Foundations of Software Science and Computational Structures","author":"M. Fiore","year":"2005","unstructured":"Fiore, M.: Mathematical models of computational and combinatorial structures. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol.\u00a03441, pp. 25\u201346. Springer, Heidelberg (2005)"},{"key":"26_CR10","unstructured":"Fiore, M.: A mathematical theory of substitution and its applications to syntax and semantics. In: Invited tutorial for the Workshop on Mathematical Theories of Abstraction, Substitution and Naming in Computer Science, ICMS (2007)"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Fiore, M.: Second-order and dependently-sorted abstract syntax. In: LICS 2008, pp. 57\u201368 (2008)","DOI":"10.1109\/LICS.2008.38"},{"key":"26_CR12","doi-asserted-by":"publisher","first-page":"1704","DOI":"10.1016\/j.tcs.2008.12.052","volume":"410","author":"M. Fiore","year":"2008","unstructured":"Fiore, M., Hur, C.-K.: On the construction of free algebras for equational systems. Theor. Comput. Sci.\u00a0410, 1704\u20131729 (2008)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Fiore, M., Hur, C.-K.: Term equational systems and logics. In: MFPS XXIV. ENTCS, vol.\u00a0218, pp. 171\u2013192 (2008)","DOI":"10.1016\/j.entcs.2008.10.011"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Fiore, M., Mahmoud, O.: Second-order algebraic theories. In: Hlineny, P. (ed.) MFCS 2010. LNCS, vol.\u00a06281, pp. 368\u2013380. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-15155-2_33"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: LICS 1999, pp. 193\u2013202 (1999)","DOI":"10.1109\/LICS.1999.782615"},{"key":"26_CR16","first-page":"307","volume":"11","author":"J. Goguen","year":"1985","unstructured":"Goguen, J., Meseguer, J.: Completeness of many-sorted equational logic. Houston J. Math.\u00a011, 307\u2013334 (1985)","journal-title":"Houston J. Math."},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Hamana, M.: Term rewriting with variable binding: An initial algebra approach. In: PPDP 2003, pp. 148\u2013159 (2003)","DOI":"10.1145\/888251.888266"},{"key":"26_CR18","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_CR19","unstructured":"Hur, C.-K.: Categorical Equational Systems: Algebraic Models and Equational Reasoning. PhD thesis, Computer Laboratory, University of Cambridge (2010)"},{"issue":"4","key":"26_CR20","first-page":"61","volume":"9","author":"G. Janelidze","year":"2001","unstructured":"Janelidze, G., Kelly, G.: A note on actions of a monoidal category. TAC\u00a09(4), 61\u201391 (2001)","journal-title":"TAC"},{"key":"26_CR21","unstructured":"Klop, J.: Combinatory Reduction Systems. PhD thesis, Mathematical Centre Tracts 127, CWI, Amsterdam (1980)"},{"key":"26_CR22","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"J. Klop","year":"1993","unstructured":"Klop, J., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theor. Comput. Sci.\u00a0121, 279\u2013308 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR23","unstructured":"Lawvere, F.: Functorial semantics of algebraic theories. Republished in: Reprints in TAC\u00a0(5), 1\u2013121 (2004)"},{"issue":"6","key":"26_CR24","doi-asserted-by":"publisher","first-page":"1455","DOI":"10.1093\/logcom\/exp033","volume":"19","author":"M.J. Gabbay","year":"2009","unstructured":"Gabbay, M.J., Mathijssen, A.: Nominal (universal) algebra: Equational logic with names and binding. J. Logic Computation\u00a019(6), 1455\u20131508 (2009)","journal-title":"J. Logic Computation"},{"key":"26_CR25","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/BF01053036","volume":"55","author":"D. Pigozzi","year":"1995","unstructured":"Pigozzi, D., Salibra, A.: The abstract variable-binding calculus. Studia Logica\u00a055, 129\u2013179 (1995)","journal-title":"Studia Logica"},{"key":"26_CR26","unstructured":"Plotkin, G.: Binding algebras: A step from universal algebra to type theory. Invited talk at RTA 1998 (1998)"},{"key":"26_CR27","unstructured":"Sun, Y.: A Framework for Binding Operators. PhD thesis, LFCS, The University of Edinburgh (1992)"},{"key":"26_CR28","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/S0304-3975(97)00170-9","volume":"211","author":"Y. Sun","year":"1999","unstructured":"Sun, Y.: An algebraic generalization of Frege structures \u2014 binding algebras. Theor. Comput. Sci.\u00a0211, 189\u2013232 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR29","unstructured":"van Raamsdonk, F.: Higher-order rewriting. In: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol.\u00a055, pp. 588\u2013667 (2003)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15205-4_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,24]],"date-time":"2025-02-24T09:29:03Z","timestamp":1740389343000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15205-4_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642152047","9783642152054"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15205-4_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}