{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,6]],"date-time":"2023-05-06T07:09:43Z","timestamp":1683356983194},"reference-count":42,"publisher":"Elsevier BV","issue":"1-3","license":[{"start":{"date-parts":[[2006,8,1]],"date-time":"2006-08-01T00:00:00Z","timestamp":1154390400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":2578,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2006,8]]},"DOI":"10.1016\/j.tcs.2006.05.033","type":"journal-article","created":{"date-parts":[[2006,7,4]],"date-time":"2006-07-04T20:27:15Z","timestamp":1152044835000},"page":"415-439","source":"Crossref","is-referenced-by-count":3,"title":["Interfaces as functors, programs as coalgebras\u2014A final coalgebra theorem in intensional type theory"],"prefix":"10.1016","volume":"360","author":[{"given":"Markus","family":"Michelbrink","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.tcs.2006.05.033_bib1","first-page":"23","article-title":"Categories of containers","volume":"Vol. 2620","author":"Abbott","year":"2003"},{"key":"10.1016\/j.tcs.2006.05.033_bib2","first-page":"16","article-title":"Derivatives of containers","volume":"Vol. 2701","author":"Abbott","year":"2003"},{"issue":"1\u20132","key":"10.1016\/j.tcs.2006.05.033_bib3","first-page":"1","article-title":"\u2202 for data","volume":"65","author":"Abbott","year":"2005","journal-title":"Fund. Inform."},{"key":"10.1016\/j.tcs.2006.05.033_bib4","doi-asserted-by":"crossref","unstructured":"M.G. Abbott, Categories of containers, Ph.D. Thesis, University of Leicester, 2003.","DOI":"10.1007\/3-540-36576-1_2"},{"issue":"2","key":"10.1016\/j.tcs.2006.05.033_bib5","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1017\/S0956796802004501","article-title":"Setoids in type theory","volume":"13","author":"Barthe","year":"2003","journal-title":"J. Funct. Programming"},{"key":"10.1016\/j.tcs.2006.05.033_bib6","unstructured":"V. Capretta, Abstraction and computation: type theory, algebraic structures, and recursive functions, Ph.D. Thesis, University of Nijmegen, 2002."},{"key":"10.1016\/j.tcs.2006.05.033_bib7","unstructured":"C. Coquand, Agda, Internet, URL \u3008www.cs.chalmers.se\/catarina\/agda\/\u3009."},{"key":"10.1016\/j.tcs.2006.05.033_bib8","doi-asserted-by":"crossref","unstructured":"T. Coquand, Infinite objects in type theory, in: H. Barendregt, T. Nipkow (Eds.), Selected Papers of the First Internat. Workshop on Types for Proofs and Programs, TYPES\u201993, Nijmegen, The Netherlands, 24\u201328 May 1993, Vol. 806, Springer, Berlin, 1994, pp. 62\u201378. URL \u3008citeseer.ist.psu.edu\/107677.html\u3009.","DOI":"10.1007\/3-540-58085-9_72"},{"key":"10.1016\/j.tcs.2006.05.033_bib9","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1007\/BF01211308","article-title":"Inductive families","volume":"6","author":"Dybjer","year":"1994","journal-title":"Formal Aspects of Comput."},{"issue":"2","key":"10.1016\/j.tcs.2006.05.033_bib10","doi-asserted-by":"crossref","first-page":"525","DOI":"10.2307\/2586554","article-title":"A general formulation of simultaneous inductive\u2013recursive definitions in type theory","volume":"65","author":"Dybjer","year":"2000","journal-title":"J. Symbolic Logic"},{"issue":"4","key":"10.1016\/j.tcs.2006.05.033_bib11","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1017\/S095679680200446X","article-title":"Verifications of non-functional programs using interpretations in type theory","volume":"13","author":"Filliatre","year":"2003","journal-title":"J. Funct. Programming"},{"key":"10.1016\/j.tcs.2006.05.033_bib12","article-title":"Wellfounded trees and dependent polynomial functors","volume":"Vol. 3085","author":"Gambino","year":"2004"},{"key":"10.1016\/j.tcs.2006.05.033_bib13","series-title":"Informal Proc. 1992 Workshop on Types for Proofs and Programs","first-page":"183","article-title":"Inductive and coinductive types with iteration and recursion","author":"Geuvers","year":"1992"},{"key":"10.1016\/j.tcs.2006.05.033_bib14","first-page":"39","article-title":"Codifying guarded definitions with recursive schemes","volume":"Vol. 996","author":"Gimen\u00e9z","year":"1994"},{"key":"10.1016\/j.tcs.2006.05.033_bib15","doi-asserted-by":"crossref","unstructured":"P. Hancock, P. Hyvernat, Programming interfaces and basic topology, Annals of Pure and Applied Logic 137 (1\u20133) (2006) 189\u2013239.","DOI":"10.1016\/j.apal.2005.05.022"},{"key":"10.1016\/j.tcs.2006.05.033_bib16","unstructured":"P. Hancock, A. Setzer, The IO monad in dependent type theory, in: Electronic Proc. Workshop on Dependent Types in Programming, G\u00f6teborg, 27\u201328 March, 1999, URL \u3008www.md.chalmers.se\/Cs\/Research\/Semantics\/APPSEM\/dtp99.html\u3009."},{"key":"10.1016\/j.tcs.2006.05.033_bib17","doi-asserted-by":"crossref","unstructured":"P. Hancock, A. Setzer, Interactive programs in dependent type theory, in: P. Clote, H. Schwichtenberg (Eds.), Proc. 14th Annu. Conf. of EACSL, CSL\u201900, Fischbau, Germany, 21\u201326 August 2000, Vol. 1862, Springer, Berlin, 2000, pp. 317\u2013331, URL \u3008citeseer.ist.psu.edu\/article\/hancock00interactive.html\u3009.","DOI":"10.1007\/3-540-44622-2_21"},{"key":"10.1016\/j.tcs.2006.05.033_bib18","unstructured":"P. Hancock, A. Setzer, Specifying interactions with dependent types, in: Workshop on Subtyping and Dependent Types in Programming, Portugal, 7 July 2000, 2000, electronic proceedings, URL \u3008www-sop.inria.fr\/oasis\/DTP00\/Proceedings\/proceedings.html\u3009."},{"key":"10.1016\/j.tcs.2006.05.033_bib19","doi-asserted-by":"crossref","unstructured":"P. Hancock, A. Setzer, Interactive programs and weakly final coalgebras in dependent type theory, in: L. Crosilla, P. Schuster (Eds.), From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics, Oxford Logic Guides, Clarendon Press, 2005, URL \u3008www.cs.swan.ac.uk\/\u223ccsetzer\/\u3009.","DOI":"10.1093\/acprof:oso\/9780198566519.003.0007"},{"issue":"4","key":"10.1016\/j.tcs.2006.05.033_bib20","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1017\/S0956796898003153","article-title":"A coherence theorem for Martin-L\u00f6f's type theory","volume":"8","author":"Hedberg","year":"1998","journal-title":"J. Funct. Programming"},{"key":"10.1016\/j.tcs.2006.05.033_bib21","unstructured":"M. Hofmann, Extensional concepts in intensional type theory, Ph.D. Thesis, University of Edinburg, 1995."},{"key":"10.1016\/j.tcs.2006.05.033_bib22","series-title":"Proc. Ninth Symp. on Logic in Computer Science, Paris","article-title":"A groupoid model refutes uniqueness of identity proofs","author":"Hofmann","year":"1994"},{"key":"10.1016\/j.tcs.2006.05.033_bib23","article-title":"Predicate transformers and linear logic: yet another denotational model","volume":"Vol. 3210","author":"Hyvernat","year":"2004"},{"key":"10.1016\/j.tcs.2006.05.033_bib24","series-title":"Games for Logic and Programming Languages, GaLoP (ETAPS 2005)","first-page":"1","article-title":"Synchronous games, simulations and \u03bb-calculus","author":"Hyvernat","year":"2005"},{"issue":"2","key":"10.1016\/j.tcs.2006.05.033_bib25","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","article-title":"Proving the correctness of multiprocess programs","volume":"3","author":"Lamport","year":"1977","journal-title":"IEEE Trans. Software Eng."},{"issue":"1","key":"10.1016\/j.tcs.2006.05.033_bib26","doi-asserted-by":"crossref","first-page":"57","DOI":"10.2307\/2275015","article-title":"A construction of non-wellfounded sets within Martin-L\u00f6f's type theory","volume":"54","author":"Lindstr\u00f6m","year":"1989","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/j.tcs.2006.05.033_bib27","doi-asserted-by":"crossref","unstructured":"Z. Luo, Coercive subtyping, J. Logic and Comput. 9 (1) (97\u201313) (1999) 105\u2013130.","DOI":"10.1093\/logcom\/9.1.105"},{"key":"10.1016\/j.tcs.2006.05.033_bib28","series-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"10.1016\/j.tcs.2006.05.033_bib29","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f, Mathematics of infinity, in: P. Martin-L\u00f6f, G. Mints (Eds.), COLOG-88, Internat. Conf. on Computer Logic, Tallinn, USSR, December 1988, Proceedings, Lecture Notes in Computer Science, Vol. 417, Springer, Berlin, 1990, pp. 147\u2013197.","DOI":"10.1007\/3-540-52335-9_54"},{"key":"10.1016\/j.tcs.2006.05.033_bib30","series-title":"Twenty-Five Years of Constructive Type Theory","article-title":"An intuitionistic theory of types","author":"Martin-L\u00f6f","year":"1998"},{"key":"10.1016\/j.tcs.2006.05.033_bib31","unstructured":"C. McBride, Dependently typed functional programs and their proofs, Ph.D. Thesis, University of Edinburg, 1999."},{"key":"10.1016\/j.tcs.2006.05.033_bib32","doi-asserted-by":"crossref","unstructured":"M. Michelbrink, Verifications of final coalgebra theorem in: Interfaces as Functors, Programs as Coalgebras\u2014A Final Coalgebra Theorem in Intensional Type Theory, 2005, URL \u3008www.cs.swan.ac.uk\/csmichel\/\u3009.","DOI":"10.1016\/j.tcs.2006.05.033"},{"key":"10.1016\/j.tcs.2006.05.033_bib33","first-page":"215","article-title":"Interfaces as games, programs as strategies","volume":"Vol. 3839","author":"Michelbrink","year":"2006"},{"key":"10.1016\/j.tcs.2006.05.033_bib34","first-page":"127","article-title":"State-dependent IO-monads in type theory","volume":"Vol. 122","author":"Michelbrink","year":"2005"},{"key":"10.1016\/j.tcs.2006.05.033_bib35","series-title":"Programming in Martin-L\u00f6f's Type Theory: An Introduction","author":"Nordstr\u00f6m","year":"1990"},{"key":"10.1016\/j.tcs.2006.05.033_bib36","series-title":"Twenty-Five Years of Constructive Type Theory","article-title":"On universes in type theory","author":"Palmgren","year":"1998"},{"key":"10.1016\/j.tcs.2006.05.033_bib37","unstructured":"K. Peterson, A programming system for type theory, Technical Report S-412 96, Chalmers University of Technology, G\u00f6teborg, 1982."},{"key":"10.1016\/j.tcs.2006.05.033_bib38","unstructured":"A. Salvesen, On information discharging and retrieval in Martin-L\u00f6f's type theory, Ph.D. Thesis, University of Oslo, 1989."},{"key":"10.1016\/j.tcs.2006.05.033_bib39","series-title":"Proc. of LICS\u2019 88, Edinburgh","article-title":"The strength of the subset type in Martin-L\u00f6f's type theory","author":"Salvesen","year":"1988"},{"key":"10.1016\/j.tcs.2006.05.033_bib40","unstructured":"G. Sambin, The Basic Picture, a structure for topology (the Basic Picture, I), 2001."},{"issue":"165","key":"10.1016\/j.tcs.2006.05.033_bib41","first-page":"59","article-title":"Proof theory of Martin-L\u00f6f type theory\u2014an overview","volume":"42","author":"Setzer","year":"2004","journal-title":"Math. et Sci. Humaines"},{"key":"10.1016\/j.tcs.2006.05.033_bib42","series-title":"Semantical Investigation into Intensional Type Theory","author":"Streicher","year":"1993"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397506003422?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397506003422?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T20:00:04Z","timestamp":1555704004000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397506003422"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,8]]},"references-count":42,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2006,8]]}},"alternative-id":["S0304397506003422"],"URL":"https:\/\/doi.org\/10.1016\/j.tcs.2006.05.033","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2006,8]]}}}