{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T16:56:58Z","timestamp":1780073818006,"version":"3.54.0"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319431437","type":"print"},{"value":"9783319431444","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-43144-4_7","type":"book-chapter","created":{"date-parts":[[2016,8,6]],"date-time":"2016-08-06T04:24:16Z","timestamp":1470457456000},"page":"107-122","source":"Crossref","is-referenced-by-count":3,"title":["Mechanical Verification of a Constructive Proof for FLP"],"prefix":"10.1007","author":[{"given":"Benjamin","family":"Bisping","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul-David","family":"Brodmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tim","family":"Jungnickel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christina","family":"Rickmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Henning","family":"Seidler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anke","family":"St\u00fcber","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Arno","family":"Wilhelm-Weidner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kirstin","family":"Peters","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Uwe","family":"Nestmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,8,7]]},"reference":[{"key":"7_CR1","series-title":"Texts in Theoretical Computer Science An EATCS Series","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2013","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science An EATCS Series. Springer, Heidelberg (2013)"},{"key":"7_CR2","unstructured":"Bisping, B., Brodmann, P.D., Jungnickel, T., Rickmann, C., Seidler, H., St\u00fcber, A., Wilhelm-Weidner, A., Peters, K., Nestmann, U.: A Constructive Proof for FLP. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/FLP.shtml . Formal proof development"},{"issue":"2","key":"7_CR3","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1145\/69624.357208","volume":"5","author":"GN Buckley","year":"1983","unstructured":"Buckley, G.N., Silberschatz, A.: An effective implementation for the generalized input-output construct of CSP. ACM Trans. Program. Lang. Syst. (TOPLAS) 5(2), 223\u2013235 (1983)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"7_CR4","unstructured":"Constable, R.L.: Effectively Nonblocking Consensus Procedures can Execute Forever - a Constructive Version of FLP. Tech. Rep. 11513, Cornell University (2011)"},{"key":"7_CR5","volume-title":"Implementig Mathematics with the Nuprl Proof Development System","author":"RL Constable","year":"1986","unstructured":"Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementig Mathematics with the Nuprl Proof Development System. Prentice-Hall, Upper Saddle River (1986)"},{"issue":"2","key":"7_CR6","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"MJ Fischer","year":"1985","unstructured":"Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM (JACM) 32(2), 374\u2013382 (1985)","journal-title":"J. ACM (JACM)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics","author":"F Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales - a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 149\u2013165. Springer, Heidelberg (1999)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/978-3-642-33475-7_15","volume-title":"Theoretical Computer Science","author":"P K\u00fcfner","year":"2012","unstructured":"K\u00fcfner, P., Nestmann, U., Rickmann, C.: Formal verification of distributed algorithms. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 209\u2013224. Springer, Heidelberg (2012)"},{"issue":"6","key":"7_CR9","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/S0020-0190(97)00040-9","volume":"61","author":"D Kumar","year":"1997","unstructured":"Kumar, D., Silberschatz, A.: A counter-example to an algorithm for the generalized input-output construct of CSP. Inform. Proc. Lett. 61(6), 287 (1997)","journal-title":"Inform. Proc. Lett."},{"issue":"2","key":"7_CR10","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1145\/279227.279229","volume":"16","author":"L Lamport","year":"1998","unstructured":"Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. (TOCS) 16(2), 133\u2013169 (1998)","journal-title":"ACM Trans. Comput. Syst. (TOCS)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"7_CR12","unstructured":"Ongaro, D., Ousterhout, J.: In Search of an Understandable Consensus Algorithm. In: Proceedings of USENIX, pp. 305\u2013320 (2014)"},{"issue":"2","key":"7_CR13","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/j.ipl.2004.06.008","volume":"92","author":"H V\u00f6lzer","year":"2004","unstructured":"V\u00f6lzer, H.: A constructive proof for FLP. Inform. Proc. Lett. 92(2), 83\u201387 (2004)","journal-title":"Inform. Proc. Lett."}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-43144-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T20:06:45Z","timestamp":1498334805000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-43144-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319431437","9783319431444"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-43144-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}