{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T07:03:55Z","timestamp":1725865435852},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319467498"},{"type":"electronic","value":"9783319467504"}],"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-46750-4_12","type":"book-chapter","created":{"date-parts":[[2016,9,20]],"date-time":"2016-09-20T22:11:57Z","timestamp":1474409517000},"page":"196-213","source":"Crossref","is-referenced-by-count":1,"title":["Soundly Proving B Method Formul\u00e6 Using Typed Sequent Calculus"],"prefix":"10.1007","author":[{"given":"Pierre","family":"Halmagrand","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-642-36742-7_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 493\u2013507. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-36742-7_34"},{"key":"12_CR3","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: shepherd your herd of provers. In: International Workshop on Intermediate Verification Languages (Boogie) (2011)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/3-540-45648-1_18","volume-title":"ZB 2002:Formal Specification and Development in Z and B","author":"J-P Bodeveix","year":"2002","unstructured":"Bodeveix, J.-P., Filali, M.: Type synthesis in B and the translation of B to PVS. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 350\u2013369. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45648-1_18"},{"key":"12_CR5","unstructured":"Boespflug, M., Carbonneaux, Q., Hermant, O.: The $$\\lambda \\varPi $$ -calculus modulo as a universal proof language. In: Proof Exchange for Theorem Proving (PxTP) (2012)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-540-75560-9_13","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R Bonichon","year":"2007","unstructured":"Bonichon, R., Delahaye, D., Doligez, D.: Zenon: an extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 151\u2013165. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-75560-9_13"},{"key":"12_CR7","unstructured":"Bury, G., Delahaye, D., Doligez, D., Halmagrand, P., Hermant, O.: Automated deduction in the B set theory using typed proof search and deduction modulo. In: LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Suva, Fiji (2015)"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Cauderlier, R., Halmagrand, P.: Checking Zenon modulo proofs in Dedukti. In: Fourth Workshop on Proof eXchange for Theorem Proving (PxTP), Berlin, Germany (2015)","DOI":"10.4204\/EPTCS.186.7"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-642-45221-5_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Delahaye","year":"2013","unstructured":"Delahaye, D., Doligez, D., Gilbert, F., Halmagrand, P., Hermant, O.: Zenon modulo: when achilles outruns the tortoise using deduction modulo. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 274\u2013290. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-45221-5_20"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1007\/978-3-662-43652-3_26","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z (ABZ)","author":"D Delahaye","year":"2014","unstructured":"Delahaye, D., Dubois, C., March\u00e9, C., Mentr\u00e9, D.: The Bware project: building a proof platform for the automated verification of B proof obligations. In: Ameur, Y.A., Schewe, K.-S. (eds.) Abstract State Machines, Alloy, B, VDM, and Z (ABZ). LNCS, vol. 8477, pp. 290\u2013293. Springer, Heidelberg (2014)"},{"key":"12_CR11","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1023\/A:1027357912519","volume":"31","author":"G Dowek","year":"2003","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving Modulo. J. Autom. Reasoning (JAR) 31, 33\u201372 (2003)","journal-title":"J. Autom. Reasoning (JAR)"},{"key":"12_CR12","unstructured":"Dowek, G., Miquel, A.: Cut elimination for zermelo set theory. Archive for Mathematical Logic. Springer, Heidelberg (2007, submitted)"},{"key":"12_CR13","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/978-3-642-24690-6_18","volume":"7041","author":"M Jacquel","year":"2011","unstructured":"Jacquel, M., Berkani, K., Delahaye, D., Dubois, C.: Verifying B proof rules using deep embedding and automated theorem proving. Softw. Eng. Formal Methods 7041, 253\u2013268 (2011)","journal-title":"Softw. Eng. Formal Methods"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-540-75560-9_22","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"\u00c9 Jaeger","year":"2007","unstructured":"Jaeger, \u00c9., Dubois, C.: Why would you trust B? In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 288\u2013302. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-75560-9_22"},{"key":"12_CR15","unstructured":"Kleene, S.C.: Permutability of inferences in Gentzens calculi LK and LJ. In: Bulletin Of The American Mathematical Society, vol. 57, pp. 485\u2013485. Amer Mathematical Soc, Providence (1951)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-642-30885-7_17","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"D Mentr\u00e9","year":"2012","unstructured":"Mentr\u00e9, D., March\u00e9, C., Filli\u00e2tre, J.-C., Asuka, M.: Discharging proof obligations from Atelier\u00a0B using multiple automated provers. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 238\u2013251. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-30885-7_17"},{"key":"12_CR17","unstructured":"Schmalz, M.: Formalizing the logic of event-B. Ph.D. thesis, Diss., Eidgen\u00f6ssische Technische Hochschule ETH Z\u00fcrich, Nr. 20516, 2012 (2012)"},{"key":"12_CR18","unstructured":"ClearSy: Atelier B 4.1 (2013). http:\/\/www.atelierb.eu\/"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46750-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T19:17:21Z","timestamp":1498331841000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46750-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319467498","9783319467504"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46750-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}