{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T14:57:48Z","timestamp":1770994668396,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540617808","type":"print"},{"value":"9783540707226","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61780-9_67","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:25:29Z","timestamp":1330295129000},"page":"135-152","source":"Crossref","is-referenced-by-count":20,"title":["An application of co-inductive types in Coq: Verification of the alternating bit protocol"],"prefix":"10.1007","author":[{"given":"Eduardo","family":"Gim\u00e9nez","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"10_CR1","unstructured":"P. Aczel. Non-Well-Founded Sets, volume 14 of CLSI Lecture Notes. Stanford University, 1988."},{"key":"10_CR2","unstructured":"M. Bezem and J. Groote. A Formal verification of Alternating Protocol in the Calculus of Constructions. Technical Report 88, Departament of Philosophy, University of Utrecht, 1993."},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"T. Coquand. Infinite objects in Type Theory. In Henk Barendregt, Tobias Nipkow, editor, Types for Proofs and Programs, pages 62\u201378. LNCS 806, 1993.","DOI":"10.1007\/3-540-58085-9_72"},{"key":"10_CR4","unstructured":"C. Cornes et al. The Coq Proof assistant user's guide \u2014 Version V5.10. Technical Report 0177, INRIA, 1995."},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"C. Cornes and D. Terrasse. Automatizing Inversion Predicates in Coq. In BRA Workshop on Types for Proofs on Programs, 1995. In this book.","DOI":"10.1007\/3-540-61780-9_64"},{"key":"10_CR6","unstructured":"M. Dummett. Elements of Intuitionism. Oxford University Press, 1977."},{"key":"10_CR7","first-page":"39","volume":"996","author":"E. Gim\u00e9nez","year":"1994","unstructured":"E. Gim\u00e9nez. Codifying guarded definitions with recursive schemes. In BRA Workshop on Types for Proofs and Programs (TYPES'94), LNCS 996, pages 39\u201359, 1994.","journal-title":"LNCS"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"L. Helmink, M.P.A. Sellink, and F.W. Vaandrager. Proof-Checking a Data Link Protocol. In Henk Barendregt, Tobias Nipkow, editor, Types for Proofs and Programs, pages 127\u2013165. LNCS 806, 1993.","DOI":"10.1007\/3-540-58085-9_75"},{"key":"10_CR9","first-page":"993","volume":"77","author":"G. Kahn","year":"1977","unstructured":"G. Kahn and D. MacQueen. Coroutines and networks of parallel processes. Information Processing 77, pages 993\u2013998, 1977.","journal-title":"Information Processing"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"L. Magnusson and B. Nordstr\u00f6m. The ALF proof editor and its proof engine. In Nijmegen Workshop on Types for Proofs and Programs, 1993.","DOI":"10.1007\/3-540-58085-9_78"},{"key":"10_CR11","first-page":"351","volume":"947","author":"C. Parent","year":"1995","unstructured":"C. Parent. Synthesizing proofs from programs in the Calculus of Inductive Constructions. In Mathematics for Programs Constructions'95, LNCS 947, pages 351\u2013379, 1995.","journal-title":"LNCS"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Inductive definitions in the system Coq: Rules and Properties. In M. Bezem, J.F. Groote, editor, Proceedings of the TLCA, 1993.","DOI":"10.1007\/BFb0037116"},{"key":"10_CR13","unstructured":"L. Paulson. Co-induction and Co-recursion in Higher-order Logic. Technical Report 304, Computer Laboratory, University of Cambridge, 1993."},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"L. Paulson. The Isabelle reference manual. Technical Report 283, Computer Laboratory, University of Cambridge, 1993.","DOI":"10.1007\/BFb0030541"},{"key":"10_CR15","unstructured":"L. Paulson. A fixed point approach to implementing (co)inductive definitions. Technical Report 304, Computer Laboratory, University of Cambridge, 1995."},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"K.V.S. Prasad. Programming with broadcasts. In E. Best, editor, CONCUR'93, pages 173\u2013187. LNCS 715, 1993.","DOI":"10.1007\/3-540-57208-2_13"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"K.V.S. Prasad. A Calculus of Broadcasting Systems. To appear in Science of Computer Programming, 1995.","DOI":"10.1016\/0167-6423(95)00017-8"},{"key":"10_CR18","unstructured":"H.P. Sanders. A Logic of Functional Programs with an Application to Concurrency. PhD thesis, Chalmers University of G\u00f6teborg, 1992."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61780-9_67.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:10:54Z","timestamp":1605647454000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61780-9_67"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617808","9783540707226"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-61780-9_67","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}