{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:25:28Z","timestamp":1767929128109,"version":"3.49.0"},"reference-count":0,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2002,11,6]],"date-time":"2002-11-06T00:00:00Z","timestamp":1036540800000},"content-version":"unspecified","delay-in-days":5,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2002,11]]},"abstract":"<jats:p>Algorithms for checking subtyping between recursive types lie at the core of many programming \nlanguage implementations. But the fundamental theory of these algorithms and how \nthey relate to simpler declarative specifications is not widely understood, due in part to the \ndifficulty of the available introductions to the area. This tutorial paper offers an \u2018end-to-end\u2019 \nintroduction to recursive types and subtyping algorithms, from basic theory to efficient \nimplementation, set in the unifying mathematical framework of coinduction.<\/jats:p>","DOI":"10.1017\/s0956796802004318","type":"journal-article","created":{"date-parts":[[2002,11,18]],"date-time":"2002-11-18T06:32:00Z","timestamp":1037601120000},"page":"511-548","source":"Crossref","is-referenced-by-count":53,"title":["Recursive subtyping revealed"],"prefix":"10.1017","volume":"12","author":[{"given":"VLADIMIR","family":"GAPEYEV","sequence":"first","affiliation":[]},{"given":"MICHAEL Y.","family":"LEVIN","sequence":"additional","affiliation":[]},{"given":"BENJAMIN C.","family":"PIERCE","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2002,11,6]]},"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796802004318","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,6]],"date-time":"2019-05-06T20:24:05Z","timestamp":1557174245000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796802004318\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,11]]},"references-count":0,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2002,11]]}},"alternative-id":["S0956796802004318"],"URL":"https:\/\/doi.org\/10.1017\/s0956796802004318","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,11]]}}}