{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T00:10:08Z","timestamp":1750810208613,"version":"3.41.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661063"},{"type":"electronic","value":"9783319661070"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66107-0_9","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"131-147","source":"Crossref","is-referenced-by-count":3,"title":["FoCaLiZe and Dedukti to the Rescue for Proof Interoperability"],"prefix":"10.1007","author":[{"given":"Rapha\u00ebl","family":"Cauderlier","sequence":"first","affiliation":[]},{"given":"Catherine","family":"Dubois","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-25379-9_12","volume-title":"Certified Programs and Proofs","author":"M Armand","year":"2011","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 135\u2013150. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-25379-9_12"},{"unstructured":"Assaf, A.: A framework for defining computational higher-order logics. Ph.D. thesis, \u00c9cole Polytechnique (2015)","key":"9_CR2"},{"doi-asserted-by":"crossref","unstructured":"Assaf, A., Burel, G.: Translating HOL to Dedukti. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, EPTCS, Berlin, Germany, 2\u20133 August 2015, vol. 186, pp. 74\u201388 (2015)","key":"9_CR3","DOI":"10.4204\/EPTCS.186.8"},{"unstructured":"Assaf, A., Burel, G., Cauderlier, R., Delahaye, D., Dowek, G., Dubois, C., Gilbert, F., Halmagrand, P., Hermant, O., Saillard, R.: Expressing theories in the $$\\lambda \\Pi $$-calculus modulo theory and in the Dedukti system (2016). http:\/\/www.lsv.ens-cachan.fr\/dowek\/Publi\/expressing.pdf","key":"9_CR4"},{"doi-asserted-by":"crossref","unstructured":"Assaf, A., Cauderlier, R.: Mixing HOL and Coq in Dedukti. In: Kaliszyk, C., Paskevich, A. (eds.) 4th Workshop on Proof eXchange for Theorem Proving, EPTCS, Berlin, Germany, 2\u20133 August 2015, vol. 186, pp. 89\u201396 (2015)","key":"9_CR5","DOI":"10.4204\/EPTCS.186.9"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-642-24364-6_2","volume-title":"Frontiers of Combining Systems","author":"JC Blanchette","year":"2011","unstructured":"Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle\/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 12\u201327. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-24364-6_2"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-22438-6_14","volume-title":"Automated Deduction \u2013 CADE-23","author":"G Burel","year":"2011","unstructured":"Burel, G.: Experimenting with deduction modulo. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 162\u2013176. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-22438-6_14"},{"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, November 2015","key":"9_CR8"},{"doi-asserted-by":"crossref","unstructured":"Cauderlier, R.: A rewrite system for proof constructivization. In: Proceedings of the 2016 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, pp. 2:1\u20132:7. ACM (2016)","key":"9_CR9","DOI":"10.1145\/2966268.2966270"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-319-46750-4_26","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2016","author":"R Cauderlier","year":"2016","unstructured":"Cauderlier, R., Dubois, C.: ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 459\u2013468. Springer, Cham (2016). doi:10.1007\/978-3-319-46750-4_26"},{"doi-asserted-by":"crossref","unstructured":"Cauderlier, R., Halmagrand, P.: Checking Zenon modulo proofs in Dedukti. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings 4th Workshop on Proof eXchange for Theorem Proving, EPTCS, Berlin, Germany, 2\u20133 August 2015, vol. 186, pp. 57\u201373 (2015)","key":"9_CR11","DOI":"10.4204\/EPTCS.186.7"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-44659-1_8","volume-title":"Theorem Proving in Higher Order Logics","author":"E Denney","year":"2000","unstructured":"Denney, E.: A prototype proof translator from HOL to Coq. In: Aagaard, M., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 108\u2013125. Springer, Heidelberg (2000). doi:10.1007\/3-540-44659-1_8"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-319-08434-3_20","volume-title":"Intelligent Computer Mathematics","author":"T Gauthier","year":"2014","unstructured":"Gauthier, T., Kaliszyk, C.: Matching concepts across HOL libraries. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 267\u2013281. Springer, Cham (2014). doi:10.1007\/978-3-319-08434-3_20"},{"key":"9_CR14","doi-asserted-by":"publisher","first-page":"4919","DOI":"10.1016\/j.tcs.2011.03.022","volume":"412","author":"F Horozal","year":"2011","unstructured":"Horozal, F., Rabe, F.: Representing model theory in a type-theoretical logical framework. Theor. Comput. Sci. 412, 4919\u20134945 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/BFb0105410","volume-title":"Theorem Proving in Higher Order Logics","author":"DJ Howe","year":"1996","unstructured":"Howe, D.J.: Importing mathematics from HOL into Nuprl. In: Goos, G., Hartmanis, J., Leeuwen, J., Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 267\u2013281. Springer, Heidelberg (1996). doi:10.1007\/BFb0105410"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-03545-1_9","volume-title":"Certified Programs and Proofs","author":"B Huffman","year":"2013","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131\u2013146. Springer, Cham (2013). doi:10.1007\/978-3-319-03545-1_9"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-20398-5_14","volume-title":"NASA Formal Methods","author":"J Hurd","year":"2011","unstructured":"Hurd, J.: The opentheory standard theory library. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 177\u2013191. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-20398-5_14"},{"key":"9_CR18","series-title":"number 7998 in LNCS","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-39634-2_7","volume-title":"Interactive Theorem Proving","author":"C Kaliszyk","year":"2013","unstructured":"Kaliszyk, C., Krauss, A.: Scalable LCF-style proof translation. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving. number 7998 in LNCS, pp. 51\u201366. Springer, Heidelberg (2013)"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-14052-5_22","volume-title":"Interactive Theorem Proving","author":"C Keller","year":"2010","unstructured":"Keller, C., Werner, B.: Importing HOL light into Coq. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 307\u2013322. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14052-5_22"},{"doi-asserted-by":"crossref","unstructured":"Miller, D., Certificates, F.P.: Making proof universal and permanent. In: Momigliano, A., Pientka, B., Pollack, R. (eds.) Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP 2013, Boston, Massachusetts, USA, 23 September 2013, pp. 1\u20132. ACM (2013)","key":"9_CR20","DOI":"10.1145\/2503887.2503894"},{"doi-asserted-by":"crossref","unstructured":"Pessaux, F.: FoCaLiZe: inside an F-IDE. In: Dubois, C., Giannakopoulou, D., M\u00e9ry, D. (eds.) Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, EPTCS, Grenoble, France, 6 April 6 2014, vol. 149, pp. 64\u201378 (2014)","key":"9_CR21","DOI":"10.4204\/EPTCS.149.7"},{"unstructured":"Prevosto, V., Jaume, M.: Making proofs in a hierarchy of mathematical structures. In: Proceedings of Calculemus, September 2003","key":"9_CR22"},{"unstructured":"Saillard, R.: Type checking in the Lambda-Pi-Calculus modulo: theory and practice. Ph.D. thesis, MINES Paritech (2015)","key":"9_CR23"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/11916277_11","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Sch\u00fcrmann","year":"2006","unstructured":"Sch\u00fcrmann, C., Stehr, M.-O.: An executable formalization of the HOL\/Nuprl connection in the metalogical framework twelf. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS, vol. 4246, pp. 150\u2013166. Springer, Heidelberg (2006). doi:10.1007\/11916277_11"},{"unstructured":"Wiedijk, F.: Encoding the HOL light logic in Coq (2007, unpublished notes)","key":"9_CR25"},{"unstructured":"Zimmermann, T., Herbelin, H.: Automatic and transparent transfer of theorems along isomorphisms in the coq proof assistant. CoRR, abs\/1505.05028 (2015)","key":"9_CR26"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66107-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T23:39:00Z","timestamp":1750808340000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}