{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:12:37Z","timestamp":1725631957667},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615873"},{"type":"electronic","value":"9783540706410"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105409","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T16:17:00Z","timestamp":1320855420000},"page":"251-266","source":"Crossref","is-referenced-by-count":13,"title":["A modular coding of UNITY in COQ"],"prefix":"10.1007","author":[{"given":"Barbara","family":"Heyd","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Cr\u00e9gut","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"F. Andersen, K.D. Petersen, and J.S. Petterson. Program verification using HOL-UNITY. In J.J. Joyce and C.-J.H. Seger, editors, International Workshop on Higher Order Logic Theorem Proving and its Applications, pages 1\u201316, Vancouver, Canada, August 1993. University of British Columbia, Springer Verlag, Lecture Notes in Computer Science, No. 780, published 1994.","DOI":"10.1007\/3-540-57826-9_121"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Na\u00efma Brown and Dominique Mery. A proof environment for concurrent programs. In FME'93: Industrial-Strength Formal Methods, number 670 in LNCS, pages 196\u2013215, 1993.","DOI":"10.1007\/BFb0024647"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Th. Coquand and G. Huet. The calculus of constructions. Information and Computation, (76):95\u2013120, 1988.","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"17_CR4","unstructured":"Boutheina Chetali. Formal verification of concurrent programs: How to specify Unity using the Larch Prover. Technical Report 2475, INRIA Lorraine, 1995."},{"key":"17_CR5","volume-title":"Parallel Program Design","author":"K.M. Chandy","year":"1989","unstructured":"K.M. Chandy and J. Misra. Parallel Program Design. Addison-Wesley, Austin, Texas, May 1989."},{"key":"17_CR6","unstructured":"Projet Coq. The Coq Proof Assistant Reference Manual. INRIA Rocquencourt and ENS Lyon, version 5.10 edition, 1994."},{"issue":"9","key":"17_CR7","doi-asserted-by":"publisher","first-page":"1005","DOI":"10.1109\/32.58787","volume":"16","author":"D.M. Goldschlag","year":"1990","unstructured":"D.M. Goldschlag. Mechanically verifying concurrent programs with the Boyer-Moore prover. IEEE Transactions on Software Engineering, 16(9):1005\u20131022, September 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"17_CR8","unstructured":"Leslie Lamport. A temporal logic of actions. Technical Report SRC-57, Digital Equipment Corporation, 1990."},{"key":"17_CR9","unstructured":"Jayadev Misra. Closure properties. unpublished manuscript on a new version of Unity, electronic version available under http:\/\/www.cs.utexas.edu\/users\/psp\/newunity.html, 1994."},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"P\u00e4ppinghaus. On the logic of UNITY. Theoretical Computer Science, 139, 1995.","DOI":"10.1016\/0304-3975(94)00043-I"},{"key":"17_CR11","unstructured":"I.S.W.B. Prasetya. Mechanically Suported Design of Self-stabilizing Algorithms. PhD thesis, University of Utrecht, october 1995."},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"J. R. Rao. Extensions of the UNITY Methodology. Number 908 in LNCS. Springer Verlag, 1995.","DOI":"10.1007\/3-540-59173-7"},{"issue":"2","key":"17_CR13","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/BF01898402","volume":"3","author":"B. Sanders","year":"1991","unstructured":"Beverly Sanders. Eliminating the substitution axiom from UNITY logic. Formal Aspects of Computing, 3(2):189\u2013205, 1991.","journal-title":"Formal Aspects of Computing"},{"issue":"12","key":"17_CR14","doi-asserted-by":"publisher","first-page":"1515","DOI":"10.1109\/12.9730","volume":"37","author":"M. G. Staskaukas","year":"1988","unstructured":"Mark G. Staskaukas. The formal specification and design of a distributed electronic funds-transfer system. IEEE Trans. on Computers, 37(12):1515\u20131528, December 1988.","journal-title":"IEEE Trans. on Computers"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0105409","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,19]],"date-time":"2019-06-19T05:44:15Z","timestamp":1560923055000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105409"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0105409","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}