{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T06:50:21Z","timestamp":1760079021497,"version":"3.30.2"},"reference-count":33,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,7,1]],"date-time":"2003-07-01T00:00:00Z","timestamp":1057017600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3681,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,7]]},"DOI":"10.1016\/s1571-0661(04)80639-x","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T16:47:47Z","timestamp":1096476467000},"page":"191-205","source":"Crossref","is-referenced-by-count":7,"title":["Substitution in Non-wellfounded Syntax with Variable Binding"],"prefix":"10.1016","volume":"82","author":[{"given":"Ralph","family":"Matthes","sequence":"first","affiliation":[]},{"given":"Tarmo","family":"Uustalu","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB1","series-title":"Selected Papers from 2nd Int. Wksh. on Types for Proofs and Programs, TYPES'02 (Berg en Dal near Nijmegen, Apr. 2002)","first-page":"1","article-title":"(Co-)interation for higher-order nested datatypes","author":"Abel","year":"2003"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB2","series-title":"Proc. of 6th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS'03 (Warsaw, Apr. 2003)","first-page":"54","article-title":"Generalized iteration and coiteration for higher-order nested datatypes","author":"Abel","year":"2003"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB3","doi-asserted-by":"crossref","unstructured":"Aczel P., Frege structures and the notions of proposition, truth and set, in: J. Barwise, H. J. Keisler and K. Kunen, eds., Proc. of The Kleene Symp. (Madison, WI, June 1978), Studies in Logic and Found. of Math. 101, North Holland, Amsterdam, 1980 pp. 31\u201359.","DOI":"10.1016\/S0049-237X(08)71252-7"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB4","series-title":"Revised Lectures from Int. Summer School and Wksh. on Algebraic and Coalgebraic Methods in the Mathematics of Program Construction (Oxford, April 2000)","first-page":"79","article-title":"Algebras and coalgebras","author":"Aczel","year":"2002"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB5","doi-asserted-by":"crossref","unstructured":"Aczel, P. J., Ad\u00e1mek and J. Velebil, A coalgebraic view of infinite trees and iteration, in: A. Corradini, M. Lenisa and U. Montanari, eds., Proc. of 4th Wksh. on Coalgebraic Methods in Computer Science, CMCS'01 (Genova, Apr. 2001), Electr. Notes in Theoret. Comput. Sci. 44(1), Elsevier, Amsterdam, 2001. Journal version with S. Milius as an additional coauthor to appear in Theoret. Comput. Sci.","DOI":"10.1016\/S1571-0661(04)80900-9"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB6","doi-asserted-by":"crossref","unstructured":"Aehlig K. and F. Joachimski, On continuous normalization, in: J. C. Bradfield, ed., Proc. of 16th Int. Wksh. on Computer Science Logic, CSL 2002 (Edinburgh, Sept. 2002), Lect. Notes in Comput. Sci. 2471, Springer-Verlag, Berlin, 2002 pp. 59\u201373.","DOI":"10.1007\/3-540-45793-3_5"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB7","doi-asserted-by":"crossref","unstructured":"Altenkirch T. and B. Reus, Monadic presentations of lambda terms using generalized inductive types, in: J. Flum and M. Rodr\u00edguez-Artalejo, eds., Proc. of 13th Int. Wksh. on Computer Science Logic, CSL'99 (Madrid, Sept. 1999), Lect. Notes in Comput. Sci. 1683, Springer-Verlag, Berlin, 1999 pp. 453\u2013468.","DOI":"10.1007\/3-540-48168-0_32"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB8","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/BF01111838","article-title":"Coequalizers and free triples","volume":"116","author":"Barr","year":"1970","journal-title":"Math. Z"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB9","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/0167-6423(94)00022-0","article-title":"Substitution: A formal methods case study using monads and transformations","volume":"23","author":"Bellegarde","year":"1994","journal-title":"Sci. of Comput. Program"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB10","doi-asserted-by":"crossref","unstructured":"Bird R. and L. Meertens, Nested datatypes, in: J. Jeuring, ed., Proc. of 4th Int. Conf. on Mathematics of Program Construction, MPC'98 (Marstrand, June 1998), Lect. Notes in Comput. Sci. 1422, Springer-Verlag, Berlin, 1998 pp. 52\u201367.","DOI":"10.1007\/BFb0054285"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB11","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/s001650050047","article-title":"Generalised folds for nested datatypes","volume":"11","author":"Bird","year":"1999","journal-title":"Formal Aspects of Computing"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB12","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1017\/S0956796899003366","article-title":"De Bruijn notation as a nested datatype","volume":"9","author":"Bird","year":"1999","journal-title":"J. of Functional Programming"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB13","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","article-title":"Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with applications to the Church-Rosser theorem","volume":"34","author":"de Bruijn","year":"1972","journal-title":"Indagationes Math"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB14","unstructured":"Crole, R. L., Basic category theory for models of syntax, Course notes for Summer School on Generic Programming, SSGP'02 (Oxford, Aug. 2002), to appear."},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB15","doi-asserted-by":"crossref","unstructured":"Fiore M., G. D. Plotkin and D. Turi, Abstract syntax and variable binding (extended abstract), in: Proc. of 14th Ann. IEEE Symp. on Logic in Computer Science, LICS'99 (Trento, July 1999), IEEE CS Press, Los Alamitos, CA, 1999, pp. 193\u2013202.","DOI":"10.1109\/LICS.1999.782615"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB16","doi-asserted-by":"crossref","unstructured":"Ghani N., C. L\u00fcth and F. de Marchi, Coalgebraic monads, in: L. S. Moss, ed., Proc. of 5th Wksh. on Coalgebraic Methods in Computer Science, CMCS'02 (Grenoble, Apr. 2002), Electr. Notes in Theoret. Comput. Science 65.1, Elsevier, Amsterdam, 2002.","DOI":"10.1016\/S1571-0661(04)80360-8"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB17","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1017\/S0960129502003912","article-title":"Dualising initial algebras","volume":"13","author":"Ghani","year":"2003","journal-title":"Math. Struct. in Comput. Sci"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB18","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1017\/S096012950100336X","article-title":"Locus solum: From the rules of logic to the logic of rules","volume":"11","author":"Girard","year":"2001","journal-title":"Math. Struct. in Comput. Sci"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB19","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","article-title":"A framework for defining logics","volume":"40","author":"Harper","year":"1993","journal-title":"J. of ACM"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB20","first-page":"193","article-title":"Polytypic functions over nested datatypes","volume":"3","author":"Hinze","year":"1999","journal-title":"Discrete Math. and Theoret. Comput. Sci"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB21","doi-asserted-by":"crossref","unstructured":"Hofmann M., Semantical analysis of higher-order abstract syntax, in: Proc. of 14th Ann. IEEE Symp. on Logic in Computer Science, LICS'99 (Trento, July 1999), IEEE CS Press, Los Alamitos, CA, 1999 pp. 204\u2013213.","DOI":"10.1109\/LICS.1999.782616"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB22","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/S0304-3975(96)00171-5","article-title":"Infinitary lambda calculus","volume":"175","author":"Kennaway","year":"1997","journal-title":"Theoret. Comput. Sci"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB23","unstructured":"Matthes R., Monotone inductive and coinductive constructors of rank 2, in: L. Fribourg, ed., Proc. of 15th Int. Wksh. on Computer Science Logic, CSL'01 (Paris, Sept. 2001), Lect. Notes in Comput. Sci. 2142, Springer-Verlag, Berlin, 2001 pp. 600\u2013614."},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB24","unstructured":"Mints, G., Finite investigations of infinite derivations, Zap. Nauchn. Semin. Leningr. Otd. Matem. Inst. 49 (1975). Translation in: J. of Soviet Math. 10 (1978), pp. 548\u2013596. Reprinted in: Mints, G., \u201cSelected Papers in Proof Theory\u201d, Studies in Proof Theory: Monographs 3, Bibliopolis, Napoli, 1992 pp. 17\u201372."},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB25","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/S0168-0072(00)00011-7","article-title":"Reduction of finite and infinite derivations","volume":"104","author":"Mints","year":"2000","journal-title":"Ann. of Pure and Appl. Logic"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB26","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1016\/S0304-3975(00)00126-2","article-title":"Parametric corecursion","volume":"260","author":"Moss","year":"2001","journal-title":"Theoret. Comput. Sci"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB27","doi-asserted-by":"crossref","unstructured":"Okasaki C., From fast exponentiation to square matrices: An adventure in types, in: Proc. of 5th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP'99 (Paris, Sept. 1999), ACM Press, New York, 1999 pp. 28\u201335.","DOI":"10.1145\/317636.317781"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB28","doi-asserted-by":"crossref","unstructured":"Pfenning F. and C. Elliot, Higher-order abstract syntax, in: Proc. of ACM SIGPLAN 1988 Conf. on Programming Language Design and Implementation, PLDI'88 (Atlanta, GA, June 1988), ACM Press, New York, 1988 pp. 199\u2013208.","DOI":"10.1145\/53990.54010"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB29","series-title":"Situation Theory and Its Applications, Vol. 1","first-page":"133","article-title":"An illative theory of relations","author":"Plotkin","year":"1990"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB30","doi-asserted-by":"crossref","unstructured":"Severi P., and F.-J. de Vries, An extensional B\u00f6hm model, in: S. Tison, ed., Proc. of 13th Int. Conf. on Rewriting Theory and Applications, RTA 2002 (Copenhagen, July 2002), Lect. Notes in Comput. Sci. 2378, Springer-Verlag, Berlin, 2002 pp. 159\u2013173.","DOI":"10.1007\/3-540-45610-4_12"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB31","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/S0304-3975(97)00170-9","article-title":"An algebraic generalization of Frege structures - binding signatures","volume":"211","author":"Sun","year":"1999","journal-title":"Theoret. Comput. Sci"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB32","series-title":"Prel. Proc. of 4th Int. Wksh. Fixed Points in Computer Science, FICS'02 (Copenhagen, July 2002)","first-page":"9","article-title":"Generalizing substitution (extended abstract)","author":"Uustalu","year":"2002"},{"key":"10.1016\/S1571-0661(04)80639-X_NEWBIB33","first-page":"5","article-title":"Primitive (co)recursion and course-of-value (co)iteration, categorically","volume":"10","author":"Uustalu","year":"1999","journal-title":"Informatica"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610480639X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610480639X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,12,18]],"date-time":"2024-12-18T20:06:45Z","timestamp":1734552405000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S157106610480639X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,7]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,7]]}},"alternative-id":["S157106610480639X"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80639-x","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2003,7]]}}}