{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:01:16Z","timestamp":1754481676299},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540580850"},{"type":"electronic","value":"9783540484400"}],"license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58085-9_75","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:11:30Z","timestamp":1330269090000},"page":"127-165","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":68,"title":["Proof-checking a data link protocol"],"prefix":"10.1007","author":[{"given":"L.","family":"Helmink","sequence":"first","affiliation":[]},{"given":"M. P. A.","family":"Sellink","sequence":"additional","affiliation":[]},{"given":"F. W.","family":"Vaandrager","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/BF01872848","volume":"2","author":"K. Apt","year":"1988","unstructured":"K. Apt, N. Francez, and S. Katz. Appraising fairness in languages for distributed programming. Distributed Computing, 2:226\u2013241, 1988.","journal-title":"Distributed Computing"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"H. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, pages 117\u2013309. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"7_CR3","unstructured":"M. Bezem and J. Groote. A formal verification of the alternating bit protocol in the calculus of constructions. Logic Group Preprint Series 88, Dept. of Philosophy, Utrecht University, Mar. 1993."},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"G. v. Bochmann and D. Probst, editors. Proceedings of the 4th International Conference on Computer Aided Verification, volume 663 of Lecture Notes in Computer Science. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-56496-9"},{"key":"7_CR5","volume-title":"Report CS-R94XX","author":"D. Bosscher","year":"1994","unstructured":"D. Bosscher, I. Polak, and F. Vaandrager. Verification of an audio control protocol. Report CS-R94XX, CWI, Amsterdam, 1994. In preparation."},{"key":"7_CR6","unstructured":"CCITT Fascicle VIII.3. CCITT Recommendation X.25. Interface between DTE and DCE for Terminals Operating in the Packet Mode on Public Data Networks, 1988."},{"issue":"15","key":"7_CR7","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/151646.151648","volume":"1","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench: A semantics based tool for the verification of concurrent systems. ACM Trans. Prog. Lang. Syst., 1(15):36\u201372, 1993.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"volume-title":"volume 697 of Lecture Notes in Computer Science","year":"1993","key":"7_CR8","unstructured":"C. Courcoubetis, editor. Proceedings of the 5th International Conference on Computer Aided Verification, Elounda, Greece, June\/July 1993, volume 697 of Lecture Notes in Computer Science. Springer-Verlag, 1993."},{"key":"7_CR9","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, INRIA \u2014 Rocquencourt, May 1993."},{"key":"7_CR10","unstructured":"U. Engberg, P. Gr\u00f8nning, and L. Lamport. Mechanical verification of concurrent systems with TLA. In Bochmann and Probst [4]."},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"M. Gordon. HOL: a proof generating system for higher-order logic. In G. Birtwistle and P. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis. Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"7_CR12","unstructured":"J. Groote and J. van de Pol. A bounded retransmission protocol for large data packets. Logic Group Preprint Series 100, Dept. of Philosophy, Utrecht University, Oct. 1993."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"J. Guttag and J. Horning. Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993.","DOI":"10.1007\/978-1-4612-2704-5"},{"key":"7_CR14","unstructured":"M. Hofmann. Extensional Concepts in Intensional Type Theory. PhD thesis, University of Edinburgh, 1994. Forthcoming."},{"key":"7_CR15","unstructured":"B. Jonsson. Compositional Verification of Distributed Systems. PhD thesis, Department of Computer Systems, Uppsala University, 1987. DoCS 87\/09."},{"key":"7_CR16","unstructured":"L. Lamport. How to write a proof. Research Report 94, Digital Equipment Corporation, Systems Research Center, Feb. 1993."},{"key":"7_CR17","first-page":"302","volume-title":"volume 531 of Lecture Notes in Computer Science","author":"P. Loewenstein","year":"1991","unstructured":"P. Loewenstein and D. Dill. Verification of a multiprocessor cache protocol using simulation relations and higher-order logic (summary). In E. Clarke and R. Kurshan, editors, Proceedings of the 2nd International Conference on Computer-Aided Verification, New Brunswick, NJ, USA June 1990, volume 531 of Lecture Notes in Computer Science, pages 302\u2013311. Springer-Verlag, 1991."},{"key":"7_CR18","volume-title":"Technical Report LFCS-TN-27","author":"Z. Luo","year":"1989","unstructured":"Z. Luo, R. Pollack, and P. Taylor. How to use LEGO. Technical Report LFCS-TN-27, University of Edinburgh, Edinburgh, Scotland, Oct. 1989."},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"N. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the 6th Annual ACM Symposium on Principles of Distributed Computing, pages 137\u2013151, Aug. 1987. A full version is available as MIT Technical Report MIT\/LCS\/TR-387.","DOI":"10.1145\/41840.41852"},{"issue":"3","key":"7_CR20","first-page":"219","volume":"2","author":"N. Lynch","year":"1989","unstructured":"N. Lynch and M. Tuttle. An introduction to input\/output automata. CWI Quarterly, 2(3):219\u2013246, Sept. 1989.","journal-title":"CWI Quarterly"},{"key":"7_CR21","volume-title":"Report CS-R9313","author":"N. Lynch","year":"1993","unstructured":"N. Lynch and F. Vaandrager. Forward and backward simulations \u2014 part I: Untimed systems. Report CS-R9313, CWI, Amsterdam, Mar. 1993."},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"S. Mauw and G. Veltink, editors. Algebraic Specification of Communication Protocols. Cambridge Tracts in Theoretical Computer Science 36. Cambridge University Press, 1993.","DOI":"10.1017\/CBO9780511721625"},{"key":"7_CR23","first-page":"561","volume-title":"volume 430 of Lecture Notes in Computer Science","author":"T. Nipkow","year":"1990","unstructured":"T. Nipkow. Formal verification of data type refinement \u2014 theory and practice. In J. de Bakker, W. d. Roever, and G. Rozenberg, editors, Proceedings REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness, Mook, The Netherlands, May\/June 1989, volume 430 of Lecture Notes in Computer Science, pages 561\u2013591. Springer-Verlag, 1990."},{"key":"7_CR24","first-page":"328","volume-title":"volume 664 of Lecture Notes in Computer Science","author":"C. Paulin-Mohring","year":"1993","unstructured":"C. Paulin-Mohring. Inductive definitions in the system Coq. Rules and properties. In M. Bezem and J. Groote, editors, Proceedings of the 1st International Conference on Typed Lambda Calculi and Applications, TCLA'93, Utrecht, The Netherlands, volume 664 of Lecture Notes in Computer Science, pages 328\u2013345. Springer-Verlag, 1993."},{"key":"7_CR25","unstructured":"L. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science. Academic Press, 1989."},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"J. S\u00f8gaard-Andersen, S. Garland, J. Guttag, N. Lynch, and A. Pogosyants. Computer-assisted simulation proofs. In Courcoubetis [8], pages 305\u2013319.","DOI":"10.1007\/3-540-56922-7_25"},{"key":"7_CR27","volume-title":"Computer networks","author":"A. Tanenbaum","year":"1981","unstructured":"A. Tanenbaum. Computer networks. Prentice-Hall International, Englewood Cliffs, 1981."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58085-9_75","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T15:44:18Z","timestamp":1713627858000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58085-9_75"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540580850","9783540484400"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-58085-9_75","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]},"assertion":[{"value":"2 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}