{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T23:09:46Z","timestamp":1771888186690,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540755586","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75560-9_22","type":"book-chapter","created":{"date-parts":[[2007,10,6]],"date-time":"2007-10-06T01:36:46Z","timestamp":1191634606000},"page":"288-302","source":"Crossref","is-referenced-by-count":8,"title":["Why Would You Trust B?"],"prefix":"10.1007","author":[{"given":"\u00c9ric","family":"Jaeger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Catherine","family":"Dubois","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book - Assigning Programs to Meanings","author":"J.R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"22_CR2","unstructured":"The Coq development team: The Coq proof assistant reference manual. LogiCal Project (2004)"},{"key":"22_CR3","first-page":"387","volume-title":"Current Trends in Hardware Verification and Automatic Theorem Proving (Proceedings of the Workshop on Hardware Verification)","author":"M.J.C. Gordon","year":"1988","unstructured":"Gordon, M.J.C.: Mechanizing programming logics in higher-order logic. In: Birtwistle, G.M., Subrahmanyam, P.A. (eds.) Current Trends in Hardware Verification and Automatic Theorem Proving (Proceedings of the Workshop on Hardware Verification), Banff, Canada, pp. 387\u2013439. Springer, Berlin (1988)"},{"key":"22_CR4","unstructured":"Boulton, R.J., Gordon, A., Gordon, M.J.C., Harrison, J., Herbert, J., Tassel, J.V.: Experience with embedding hardware description languages in hol. In: Stavridou, V., Melham, T.F., Boute, R.T. (eds.) TPCD. IFIP Transactions, North-Holland, vol.\u00a0A-10, pp. 129\u2013156 (1992)"},{"key":"22_CR5","unstructured":"Azurat, A., Prasetya, I.: A survey on embedding programming logics in a theorem prover. Technical Report UU-CS-2002-007, Institute of Information and Computing Sciences, Utrecht University (2002)"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","first-page":"33","volume-title":"FM\u201999 - Formal Methods","author":"J.P. Bodeveix","year":"1999","unstructured":"Bodeveix, J.P., Filali, M., Mu\u00f1oz, C.: A formalization of the B-method in Coq and PVS. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol.\u00a01709, pp. 33\u201349. Springer, Heidelberg (1999)"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/BFb0053356","volume-title":"B\u201998: Recent Advances in the Development and Use of the B Method","author":"P. Chartier","year":"1998","unstructured":"Chartier, P.: Formalisation of B in Isabelle\/HOL. In: Bert, D. (ed.) B 1998. LNCS, vol.\u00a01393, pp. 66\u201382. Springer, Heidelberg (1998)"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/11541868_19","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Ridge","year":"2005","unstructured":"Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first order logic. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 294\u2013309. Springer, Heidelberg (2005)"},{"issue":"7","key":"22_CR9","doi-asserted-by":"publisher","first-page":"855","DOI":"10.3166\/tsi.23.855-878","volume":"23","author":"K. Berkani","year":"2004","unstructured":"Berkani, K., Dubois, C., Faivre, A., Falampin, J.: Validation des r\u00e8gles de base de l\u2019Atelier B. Technique et Science Informatiques\u00a023(7), 855\u2013878 (2004)","journal-title":"Technique et Science Informatiques"},{"key":"22_CR10","series-title":"Lecture Notes in Artificial Intelligence","first-page":"25","volume-title":"CADE-15","author":"H. Cirstea","year":"1998","unstructured":"Cirstea, H., Kirchner, C.: Using rewriting and strategies for describing the B predicate prover. In: Kirchner, C., Kirchner, H. (eds.) CADE-15. LNCS (LNAI), vol.\u00a01421, pp. 25\u201336. Springer, Heidelberg (1998)"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae (Proceedings), pp. 381\u2013392 (1972)","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/3-540-45610-4_14","volume-title":"Rewriting Techniques and Applications","author":"C. Liang","year":"2002","unstructured":"Liang, C., Nadathur, G.: Tradeoffs in the intensional representation of lambda terms. In: Tison, S. (ed.) RTA 2002. LNCS, vol.\u00a02378, pp. 192\u2013206. Springer, Heidelberg (2002)"},{"key":"22_CR13","unstructured":"Aydemir, B., Chargu\u00e9raud, A., Pierce, B.C., Weirich, S.: Engineering aspects of formal metatheory, Manuscript (2007)"},{"key":"22_CR14","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1017\/S0956796899003366","volume":"9","author":"R. Bird","year":"1999","unstructured":"Bird, R., Paterson, R.: De Bruijn notation as a nested datatype. Journal of Functional Programming\u00a09, 77\u201391 (1999)","journal-title":"Journal of Functional Programming"},{"key":"22_CR15","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.L., L\u00e9vy, J.J.: Explicit substitutions. Journal of Functional Programming\u00a01, 375\u2013416 (1991)","journal-title":"Journal of Functional Programming"},{"key":"22_CR16","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1145\/226643.226675","volume":"43","author":"P.L. Curien","year":"1996","unstructured":"Curien, P.L., Hardin, T., L\u00e9vy, J.J.: Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM\u00a043, 362\u2013397 (1996)","journal-title":"Journal of the ACM"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1007\/3-540-57826-9_152","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"A.D. Gordon","year":"1994","unstructured":"Gordon, A.D.: A mechanisation of name-carrying syntax up to alpha-conversion. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol.\u00a0780, pp. 413\u2013425. Springer, Heidelberg (1994)"},{"key":"22_CR18","unstructured":"Mussat, L.: Private Communication (2005)"},{"key":"22_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/3-540-44404-1_7","volume-title":"Logic for Programming and Automated Reasoning","author":"D. Delahaye","year":"2000","unstructured":"Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol.\u00a01955, pp. 85\u201395. Springer, Heidelberg (2000)"},{"key":"22_CR20","volume-title":"SEFM (Software Engineering and Formal Methods)","author":"S. Colin","year":"2005","unstructured":"Colin, S., Petit, D., Rocheteau, J., Marcano, R., Mariano, G., Poirriez, V.: BRILLANT: An open source and XML-based platform for rigourous software development. In: SEFM (Software Engineering and Formal Methods), Koblenz, Germany, AGKI (Artificial Intelligence Research Koblenz), IEEE Computer Society Press, Los Alamitos (2005) selectivity : 40\/120"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75560-9_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:24:42Z","timestamp":1619504682000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75560-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540755586"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75560-9_22","relation":{},"subject":[]}}