{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:58:31Z","timestamp":1725494311117},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_19","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T15:53:07Z","timestamp":1194623587000},"page":"227-231","source":"Crossref","is-referenced-by-count":3,"title":["Fault-Tolerant Distributed Theorem Proving"],"prefix":"10.1007","author":[{"given":"Jason","family":"Hickey","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Maria Paola Bonacina and William McCune. Distributed theorem proving by peers. In 1194 Conference on Automated Deduction (CADE12), pages 841\u2013845, 1994.","DOI":"10.1007\/3-540-58156-1_72"},{"key":"19_CR2","unstructured":"Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and Man-dayam Srivas. A Tutorial Introduction to PVS. In WIFT\u2019 95: Workshop on Industrial-Strength Formal Specification Techniques, April 1995. http:\/\/www.csl.sri.com\/sri-csl-fm.html ."},{"key":"19_CR3","unstructured":"J. Denzinger and Dirk Fuchs. Cooperation in theorem proving by loosely coupled heuristics. Technical Report SR-97-04, University of Kaiserslautern, 1997."},{"key":"19_CR4","unstructured":"R.L. Constable et.al. ImplementingMathematics in the NuPRL Proof Development System. Prentice-Hall, 1986."},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"A. Felty, D. Howe, and F. Stomp. Protocol verification in Nuprl. In CAV\u201998, Lecture Notes on Computer Science. Springer, 1998.","DOI":"10.1007\/BFb0028764"},{"key":"19_CR6","unstructured":"Mark Hayden. The Ensemble system. Technical Report TR98-1662, Cornell University, 1998."},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Jason Hickey, Nancy Lynch, and Robbert van Renesse. Specifications and proofs for Ensemble layers. In TACAS\u2019 99, March 1999.","DOI":"10.1007\/3-540-49059-0_9"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Jason J. Hickey. Nuprl-Light: An implementation framework for higher-order logics. In 14th International Conference on Automated Deduction. Springer, 1997.","DOI":"10.1007\/3-540-63104-6_37"},{"key":"19_CR9","unstructured":"Paul Bernard Jackson. Enhancing the NuPRL Proof Development System and Applying it to Computational Abstract Algebra. PhD thesis, Cornell University, January 1995."},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Christoph Kreitz, Mark Hayden, and Jason Hickey. A proof environment for the development of group communications systems. In 15th International Conference on Automated Deduction, pages 317\u2013332. Springer, 1998.","DOI":"10.1007\/BFb0054269"},{"key":"19_CR11","unstructured":"Steven P. Miller and Mandayam Srivas. Formal verification of the AAMP5 microprocessor: A case study in the industrial use of formal methods. In WIFT\u2019 95: Workshop on Industrial-Strength Formal Specification Techniques, pages 2\u201316, Boca Raton, FL, 1995."},{"key":"19_CR12","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1145\/268946.268960","volume-title":"Proc. 25th ACM Symp. Principles of Programming Languages","author":"T. Nipkow","year":"1998","unstructured":"Tobias Nipkow and David von Oheimb. Javalight is type-safe definitely. In Proc. 25th ACM Symp. Principles of Programming Languages, pages p. 161\u2013170. ACM Press, New York, 1998."},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. Objective ML: A simple object-oriented extension of ML. In ACM Symposium on Principles of Programming Languages, pages 40\u201353, 1997.","DOI":"10.1145\/263699.263707"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T04:56:28Z","timestamp":1556945788000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_19","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}