{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:15:14Z","timestamp":1759637714101},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540626886"},{"type":"electronic","value":"9783540684381"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-62688-3_29","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:49:35Z","timestamp":1330278575000},"page":"63-81","source":"Crossref","is-referenced-by-count":23,"title":["Coinductive axiomatization of recursive type equality and subtyping"],"prefix":"10.1007","author":[{"given":"Michael","family":"Brandt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fritz","family":"Henglein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"5_CR1","volume-title":"Personal communication","author":"M. Abadi","year":"1996","unstructured":"Mart\u00edn Abadi. Personal communication, September 1996. ACM State of the Art Summer School on Functional and Object-Oriented Programming in Sobotka, Poland, September 8\u201314, 1996."},{"key":"5_CR2","unstructured":"Samson Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Topics in Functional Programming, pages 65\u2013117. Addison-Wesley, 1990. Also available by anonymous ftp from theory.doc.ic.ac.uk."},{"key":"5_CR3","first-page":"104","volume-title":"Subtyping recursive types","author":"R. Amadio","year":"1991","unstructured":"R. Amadio and L. Cardelli. Subtyping recursive types. In Proc. 18th Annual ACM Symposium on Principles of Programming Languages (POPL), Orlando, Florida, pages 104\u2013118. ACM Press, January 1991."},{"issue":"4","key":"5_CR4","doi-asserted-by":"crossref","first-page":"575","DOI":"10.1145\/155183.155231","volume":"15","author":"R. M. Amadio","year":"1993","unstructured":"Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems (TOPLAS), 15(4):575\u2013631, September 1993.","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"5_CR5","volume-title":"Syntactic considerations on recursive types","author":"M. Abadi","year":"1996","unstructured":"Mart\u00edn Abadi and Marcelo P. Fiore. Syntactic considerations on recursive types. In Proc. 1996 IEEE 11th Annual Symp. on Logic in Computer Science (LICS), New Brunswick, New Jersey. IEEE Computer Society Press, June 1996."},{"key":"5_CR6","unstructured":"Zena M. Ariola and Jan Willem Klop. Equational term graph rewriting. Technical report, University of Oregon, 1995. To appear in Acta Informatica."},{"issue":"1","key":"5_CR7","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1016\/0890-5401(91)90055-7","volume":"93","author":"V. Breazu-Tannen","year":"1991","unstructured":"V. Breazu-Tannen, T. Coquand, C. Gunter, and A. Scedrov. Inheritance as implicit coercion. Information and Computation, 93(1):172\u2013221, July 1991. Presented at LICS '89.","journal-title":"Information and Computation"},{"key":"5_CR8","unstructured":"Ch. Ben-Yelles. Type assignment in the lambda-calculus: Syntax and semantics. Technical report, Department of Pure Mathematics, University College of Swansea, September 1979. Author's current address: Univ\u00e9rsit\u00e9 des Sci\u00e8nces et d\u00e9 la Technologie Houari Boumediene, Institut D'Informatique, El-Alia B.P. No. 32, Alger, Algeria."},{"key":"5_CR9","unstructured":"Luca Cardelli. Algorithm for subtyping recursive types (in Modula-3). http:\/\/www.research.digital.com\/SRC\/personal\/Luca.Cardelli\/Notes\/RecSub.txt, 1993. Originally implemented in Quest and released in 1990."},{"issue":"1","key":"5_CR10","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1016\/0890-5401(91)90020-3","volume":"92","author":"F. Cardone","year":"1991","unstructured":"F. Cardone and M. Coppo. Type inference with recursive types: Syntax and semantics. Information and Computation, 92(1):48\u201380, May 1991.","journal-title":"Information and Computation"},{"key":"5_CR11","first-page":"132","volume-title":"Coherence of subsumption","author":"P. Curien","year":"1990","unstructured":"P. Curien and G. Ghelli. Coherence of subsumption. In A. Arnold, editor, Proc. 15th Coll. on Trees in Algebra and Programming, Copenhagen, Denmark, pages 132\u2013146. Springer, May 1990."},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Thierry Coquand. Infinite objects in type theory. In Proc. Int'l Workshop on Types for Proofs and Programs, Lecture Notes in Computer Science (LNCS), pages 62\u201378. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-58085-9_72"},{"key":"5_CR13","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0304-3975(83)90059-2","volume":"25","author":"B. Courcelle","year":"1983","unstructured":"B. Courcelle. Fundamental properties of infinite trees. Theoretical Computer Science, 25:95\u2013169, 1983.","journal-title":"Theoretical Computer Science"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Andrew Gordon. Bisimilarity as a theory of functional programming. In Proceedings of the Eleventh Conference on the Mathematical Foundations of Programming Semantics (MFPS), New Orleans, March 29 to April 1, 1995, Elsevier Electronic Notes in Theoretical Computer Science, volume 1, 1995.","DOI":"10.1016\/S1571-0661(04)80013-6"},{"issue":"3","key":"5_CR15","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1016\/0167-6423(94)00004-2","volume":"22","author":"F. Henglein","year":"1994","unstructured":"Fritz Henglein. Dynamic typing: Syntax and proof theory. Science of Computer Programming (SCP), 22(3):197\u2013230, 1994.","journal-title":"Science of Computer Programming (SCP)"},{"key":"5_CR16","first-page":"29","volume":"146","author":"R. Hindley","year":"1969","unstructured":"R. Hindley. The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc., 146:29\u201360, December 1969.","journal-title":"Trans. Amer. Math. Soc."},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Furio Honsell and Marina Lenisa. Final semantics for untyped lambdacalculus. In Proc. Int'l Conf. on Typed Lambda Calculi and Applications (TLCA), volume 902 of Lecture Notes in Computer Science (LNCS), pages 249\u2013265. Springer-Verlag, 1995.","DOI":"10.1007\/BFb0014057"},{"key":"5_CR18","unstructured":"Jesper J\u00f8rgensen. A Calculus for Boxing Analysis of Polymorphically Typed Languages. PhD thesis, DIKU, University of Copenhagen, October 1995."},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Dexter Kozen, Jens Palsberg, and Michael Schwartzbach. Efficient recursive subtyping. In Proc. 20th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pages 419\u2013428. ACM, ACM Press, January 1993.","DOI":"10.1145\/158511.158700"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Dexter Kozen, Jens Palsberg, and Michael Schwartzbach. Efficient recursive subtyping. Mathematical Structures in Computer Science (MSCS), 5(1), 1995.","DOI":"10.1017\/S0960129500000657"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Marina Lenisa. Final semantics for a higher order concurrent language. In H. Kirchner, editor, Proc. Coll. on Trees in Algebra and Programming (CAAP), volume 1059 of Lecture Notes in Computer Science (LNCS), pages 102\u2013118. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61064-2_32"},{"issue":"1","key":"5_CR22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(77)90053-6","volume":"4","author":"R. Milner","year":"1977","unstructured":"Robin Milner. Fully abstract models of typed lambda-calculi. Theoretical Computer Science (TCS), 4(1):1\u201322, February 1977.","journal-title":"Theoretical Computer Science (TCS)"},{"key":"5_CR23","doi-asserted-by":"crossref","first-page":"439","DOI":"10.1016\/0022-0000(84)90023-0","volume":"28","author":"R. Milner","year":"1984","unstructured":"Robin Milner. A complete inference system for a class of regular behaviours. Journal of Computer and System Sciences (JCSS), 28:439\u2013466, 1984.","journal-title":"Journal of Computer and System Sciences (JCSS)"},{"key":"5_CR24","unstructured":"J. Morris. Lambda-Calculus Models of Programming Languages. PhD thesis, MIT, 1968."},{"issue":"1","key":"5_CR25","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/0304-3975(91)90033-X","volume":"87","author":"R. Milner","year":"1991","unstructured":"Robin Milner and Mads Tofte. Co-induction in relational semantics. Theoretical Computer Science, 87(1):209\u2013220, 1991. Note.","journal-title":"Theoretical Computer Science"},{"key":"5_CR26","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/0304-3975(94)90014-0","volume":"124","author":"A. M. Pitts","year":"1994","unstructured":"Andrew M. Pitts. A co-inducion principle for recursively defined domains. Theoretical Computer Science (TCS), 124:195\u2013219, 1994.","journal-title":"Theoretical Computer Science (TCS)"},{"issue":"2","key":"5_CR27","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1006\/inco.1996.0052","volume":"127","author":"A. M. Pitts","year":"1996","unstructured":"Andrew M. Pitts. Relational properties of domains. Information and Computation, 127(2):66\u201390, June 1996.","journal-title":"Information and Computation"},{"key":"5_CR28","unstructured":"J. Rehof. Polymorphic dynamic typing \u2014 aspects of proof theory and inference. Master's thesis, DIKU, University of Copenhagen, March 1995."},{"issue":"1","key":"5_CR29","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1145\/321312.321326","volume":"13","author":"A. Salomaa","year":"1966","unstructured":"A. Salomaa. Two complete axiom systems for the algebra of regular events. Journal of the Association for Computing Machinery (JACM), 13(1):158\u2013169, 1966.","journal-title":"Journal of the Association for Computing Machinery (JACM)"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-62688-3_29.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:14:00Z","timestamp":1605629640000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62688-3_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540626886","9783540684381"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-62688-3_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}