{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:00:22Z","timestamp":1725663622120},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540544159"},{"type":"electronic","value":"9783540476177"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54415-1_72","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:46:53Z","timestamp":1330210013000},"page":"731-749","source":"Crossref","is-referenced-by-count":6,"title":["Subtyping + extensionality: Confluence of \u03b2\u03b7top reduction in F\u2264"],"prefix":"10.1007","author":[{"given":"Pierre-Louis","family":"Curien","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giorgio","family":"Ghelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"35_CR1","unstructured":"V. Breazu-Tannen, T. Coquand, C. Gunter, A. Scedrov, Inheritance and Explicit Coercion, to appear in Information and Computation, preliminary version in Proc. Logic in Computer Science 89."},{"issue":"2","key":"35_CR2","first-page":"196","volume":"1","author":"K. Bruce","year":"1990","unstructured":"K. Bruce, G. Longo, A Modest Model of Records, Inheritance and Bounded Quantification, Information and Computation 87, 1\/2, pp.196\u2013240 (1990).","journal-title":"A Modest Model of Records, Inheritance and Bounded Quantification, Information and Computation 87"},{"key":"35_CR3","unstructured":"L. Cardelli, S. Martini, J. Mitchell, A. Scedrov, An Extension of System F with Subtyping, in these Proceedings."},{"key":"35_CR4","doi-asserted-by":"crossref","unstructured":"L. Cardelli, P. Wegner, On Understanding Types, Data Abstraction and Polymorphism, ACM Computing Surveys 17 (4) (1985).","DOI":"10.1145\/6041.6042"},{"key":"35_CR5","unstructured":"L. Cardelli, Typeful Programming, DEC SRC Research Report 45 (1989)."},{"key":"35_CR6","doi-asserted-by":"crossref","unstructured":"L. Cardelli, G. Longo, A Semantic Basis for Quest, DEC SRC Research Report 55, short version in Proc. Conf. on Lisp and Functional Programming 1990, Nice (1990).","DOI":"10.1145\/91556.91586"},{"key":"35_CR7","unstructured":"P.-L. Curien, Roberto Di Cosmo, Confluence in the typed \u03bb-calculus extended with Surjective Pairing and a Terminal Type, Proc. ICALP 91, to appear in LNCS."},{"key":"35_CR8","unstructured":"P.-L. Curien, G. Ghelli, Coherence of Subsumption, Mathematical Structures in Computer Science, to appear; short version in Proc. CAAP 90, LNCS 431."},{"key":"35_CR9","doi-asserted-by":"crossref","unstructured":"P.-L. Curien, G. Ghelli, On Confluence of Weakly Normalizing Systems, Proc. RTA 91, to appear in LNCS.","DOI":"10.1007\/3-540-53904-2_98"},{"key":"35_CR10","unstructured":"P.-L. Curien, G. Ghelli, Subtyping + Extensionality: Confluence of \u03b2\u03b7top reduction in F\u2264, long version, Technical Report, University of Pisa and LIENS, to appear (1991)."},{"key":"35_CR11","unstructured":"D. van Daalen, The Language Theory of Automath, PhD Thesis, Technical University of Eindhoven, 1980."},{"key":"35_CR12","unstructured":"G. Ghelli, Proof-theoretic Studies about a Minimal Type System Integrating Inclusion and Parametric Polymorphism, PhD Thesis, TD-6\/90, Univ. of Pisa, 1990."},{"key":"35_CR13","unstructured":"J.-L. Krivine, \u03bb-calcul, Types et Mod\u00e8les, Masson (1990)."},{"key":"35_CR14","unstructured":"A. Salvesen, The Church-Rosser Theorem for LF with \u03b2\u03b7-reduction, draft (1989)."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computer Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54415-1_72.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:54:16Z","timestamp":1605646456000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54415-1_72"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544159","9783540476177"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-54415-1_72","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}