{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:59:47Z","timestamp":1754488787969,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540605799"},{"type":"electronic","value":"9783540477709"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60579-7_6","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T20:42:53Z","timestamp":1330288973000},"page":"101-119","source":"Crossref","is-referenced-by-count":16,"title":["I\/O automata in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Nipkow","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Konrad","family":"Slind","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Martin Abadi and Leslie Lamport. The existence of refinement mappings. In Proc. 3rd IEEE Symp. Logic in Computer Science, pages 165\u2013177. IEEE Computer Society Press, 1988.","DOI":"10.1109\/LICS.1988.5115"},{"key":"6_CR2","unstructured":"Yehuda Afek, Hagit Attiya, Alan Fekete, Michael Fischer, Nancy Lynch, Yishay Mansour, Da-Wei Wang, and Lenore Zuck. Reliable communication over unreliable channels. Journal of the ACM. To appeal."},{"key":"6_CR3","unstructured":"Hagit Attiya, Alan Fekete, Michael Fischer, Nancy Lynch, Yishay Mansour, Da-Wei Wang, and Lenore Zuck. Reliable communication over unreliable channels. Draft version, 1990."},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J.Hwang. Symbolic model checking: 1020 states and beyond. In Proc. 5th IEEE Symp. Logic in Computer Science, pages 428\u2013439, 1990.","DOI":"10.1109\/LICS.1990.113767"},{"key":"6_CR5","unstructured":"G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq proof assistant user's guide version 5.8. Technical Report 154, INRIA, May 1993."},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Leen Helmink, Alex Sellink, and Frits Vaandrager. Proof-checking a data link protocol. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, volume 806 of Lect. Notes in Comp. Sci., pages 127\u2013165. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58085-9_75"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Victor Luchangco, Ekrem S\u00f6ylemez, Stephen Garland, and Nancy Lynch. Verifying timing properties of concurrent algorithms. In FORTE'94: Seventh International Conference on Formal Description Techniques for Distributed Systems and Communciations Protocols, 1994. Submitted for publication.","DOI":"10.1007\/978-0-387-34878-0_19"},{"key":"6_CR8","unstructured":"Nancy Lynch, Michael Merritt, William Weihl, and Alan Fekete. Atomic Transactions. Morgan Kaufmann Publishers, 1994."},{"issue":"3","key":"6_CR9","first-page":"219","volume":"2","author":"N. Lynch","year":"1989","unstructured":"Nancy Lynch and Mark Tuttle. An introduction to Input\/Output automata. CWI Quarterly, 2(3):219\u2013246, 1989.","journal-title":"CWI Quarterly"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow. Formal verification of data type refinement \u2014 theory and practice. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, volume 430 of Lect. Notes in Comp. Sci., pages 561\u2013591. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52559-9_79"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. A fixedpoint approach to implementing (co)inductive definitions. In Alan Bundy, editor, Proc. 12th Int. Conf. Automated Deduction, volume 814 of Lect. Notes in Comp. Sci., pages 148\u2013161. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_11"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lect. Notes in Comp. Sci. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"J\u00f8rgen S\u00f8gaard-Andersen, Stephen Garland, John Guttag, Nancy Lynch, and Anya Pogosyants. Computer-assisted simulation proofs. In Fourth Conference on Computer-Aided Verification, volume 697 of Lect. Notes in Comp. Sci., pages 305\u2013319. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_25"}],"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-60579-7_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:05:13Z","timestamp":1742598313000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60579-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540605799","9783540477709"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-60579-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}