{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T19:40:01Z","timestamp":1750534801994,"version":"3.41.0"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"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":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_16","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"255-273","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Translating Between Implicit and Explicit Versions of Proof"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Blanco","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zakaria","family":"Chihani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dale","family":"Miller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"issue":"3","key":"16_CR1","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J-M Andreoli","year":"1992","unstructured":"Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Logic Comput. 2(3), 297\u2013347 (1992)","journal-title":"J. Logic Comput."},{"issue":"8","key":"16_CR2","doi-asserted-by":"publisher","first-page":"801","DOI":"10.1109\/TC.1976.1674698","volume":"25","author":"PB Andrews","year":"1976","unstructured":"Andrews, P.B.: Refutations by matings. IEEE Trans. Comput. 25(8), 801\u2013807 (1976)","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"16_CR3","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"PB Andrews","year":"1981","unstructured":"Andrews, P.B.: Theorem proving via general matings. J. ACM 28(2), 193\u2013214 (1981)","journal-title":"J. ACM"},{"key":"16_CR4","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, PxTP 2015. EPTCS, vol. 186, Berlin, Germany, pp. 74\u201388, 2\u20133 August 2015","DOI":"10.4204\/EPTCS.186.8"},{"issue":"1","key":"16_CR5","doi-asserted-by":"publisher","first-page":"2:1","DOI":"10.1145\/2071368.2071370","volume":"13","author":"D Baelde","year":"2012","unstructured":"Baelde, D.: Least and greatest fixed points in linear logic. ACM Trans. Comput. Logic 13(1), 2:1\u20132:44 (2012)","journal-title":"ACM Trans. Comput. Logic"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-540-75560-9_9","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Baelde","year":"2007","unstructured":"Baelde, D., Miller, D.: Least and greatest fixed points in linear logic. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS, vol. 4790, pp. 92\u2013106. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-75560-9_9"},{"issue":"3","key":"16_CR7","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1023\/A:1015761529444","volume":"28","author":"H Barendregt","year":"2002","unstructured":"Barendregt, H., Barendsen, E.: Autarkic computations in formal proofs. J. Autom. Reasoning 28(3), 321\u2013336 (2002)","journal-title":"J. Autom. Reasoning"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Blanco, R., Miller, D.: Proof outlines as proof certificates: a system description. In: Cervesato, I., Sch\u00fcrmann, C. (eds.) Proceedings of the First International Workshop on Focusing. Electronic Proceedings in Theoretical Computer Science, vol. 197, pp. 7\u201314. Open Publishing Association, November 2015","DOI":"10.4204\/EPTCS.197.2"},{"key":"16_CR9","unstructured":"Boespflug, M., Carbonneaux, Q., Hermant, O.: The $$\\lambda {\\Pi }$$ -calculus modulo as a universal proof language. In: Pichardie, D., Weber, T. (eds.) Proceedings of PxTP 2012: Proof Exchange for Theorem Proving, pp. 28\u201343 (2012)"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Borras, P., Cl\u00e9ment, D., Despeyroux, T., Incerpi, J., Kahn, G., Lang, B., Pascual, V.: Centaur: the system. In: Third Annual Symposium on Software Development Environments (SDE3), Boston, pp. 14\u201324 (1988)","DOI":"10.1145\/64135.65005"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/BFb0014565","volume-title":"Theoretical Aspects of Computer Software","author":"S Boutin","year":"1997","unstructured":"Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol. 1281, pp. 515\u2013529. Springer, Heidelberg (1997). doi: 10.1007\/BFb0014565"},{"issue":"2","key":"16_CR12","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1093\/logcom\/exu030","volume":"26","author":"K Chaudhuri","year":"2016","unstructured":"Chaudhuri, K., Hetzl, S., Miller, D.: A multi-focused proof system isomorphic to expansion proofs. J. Logic Comput. 26(2), 577\u2013603 (2016)","journal-title":"J. Logic Comput."},{"key":"16_CR13","unstructured":"Chihani, Z.: Certification of First-order proofs in classical and intuitionistic logics. Ph.D. thesis, Ecole Polytechnique, August 2015"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-319-24312-2_14","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"Z Chihani","year":"2015","unstructured":"Chihani, Z., Libal, T., Reis, G.: The proof certifier Checkers. In: Nivelle, H. (ed.) TABLEAUX 2015. LNCS, vol. 9323, pp. 201\u2013210. Springer, Cham (2015). doi: 10.1007\/978-3-319-24312-2_14"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Chihani, Z., Miller, D.: Proof certificates for equality reasoning. In: Benevides, M., Thiemann, R. (eds.) Post-proceedings of LSFA 2015: 10th Workshop on Logical and Semantic Frameworks, with Applications. ENTCS, vol. 323, Natal, Brazil (2016)","DOI":"10.1016\/j.entcs.2016.06.007"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-38574-2_11","volume-title":"Automated Deduction \u2013 CADE-24","author":"Z Chihani","year":"2013","unstructured":"Chihani, Z., Miller, D., Renaud, F.: Foundational proof certificates in first-order logic. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 162\u2013177. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38574-2_11"},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"Chihani, Z., Miller, D., Renaud, F.: A semantic framework for proof evidence. J. Autom. Reasoning. doi: 10.1007\/s10817-016-9380-6","DOI":"10.1007\/s10817-016-9380-6"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-73228-0_9","volume-title":"Typed Lambda Calculi and Applications","author":"D Cousineau","year":"2007","unstructured":"Cousineau, D., Dowek, G.: Embedding pure type systems in the Lambda-Pi-Calculus modulo. In: Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 102\u2013117. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-73228-0_9"},{"key":"16_CR19","unstructured":"Davis, M.: Obvious logical inferences. In: Drinan, A. (ed.) Proceedings of the 7th International Joint Conference on Artificial Intelligence (IJCAI 1981), pp. 530\u2013531. William Kaufmann, Los Altos, August 1991"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/978-3-662-48899-7_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Dunchev","year":"2015","unstructured":"Dunchev, C., Guidi, F., Sacerdoti Coen, C., Tassi, E.: ELPI: fast, embeddable, $$\\lambda $$ Prolog interpreter. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 460\u2013468. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-48899-7_32"},{"issue":"3","key":"16_CR21","doi-asserted-by":"publisher","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R Dyckhoff","year":"1992","unstructured":"Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. J. Symbolic Logic 57(3), 795\u2013807 (1992)","journal-title":"J. Symbolic Logic"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-319-40229-1_20","volume-title":"Automated Reasoning","author":"G Ebner","year":"2016","unstructured":"Ebner, G., Hetzl, S., Reis, G., Riener, M., Wolfsteiner, S., Zivota, S.: System description: GAPT 2.0. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 293\u2013301. Springer, Cham (2016). doi: 10.1007\/978-3-319-40229-1_20"},{"key":"16_CR23","first-page":"68","volume-title":"The Collected Papers of Gerhard Gentzen","author":"G Gentzen","year":"1935","unstructured":"Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68\u2013131. North-Holland, Amsterdam (1935)"},{"issue":"2","key":"16_CR24","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1017\/S0956796800000666","volume":"3","author":"J Hannan","year":"1993","unstructured":"Hannan, J.: Extended natural semantics. J. Funct. Program. 3(2), 123\u2013152 (1993)","journal-title":"J. Funct. Program."},{"issue":"1","key":"16_CR25","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143\u2013184 (1993)","journal-title":"J. ACM"},{"key":"16_CR26","unstructured":"Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical report, Citeseer (1995)"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Harrison, J., Urban, J., Wiedijk, F.: History of interactive theorem proving. In: Siekmann, J. (ed.) Computational Logic. Handbook of the History of Logic, vol. 9, pp. 135\u2013214. North Holland (2014)","DOI":"10.1016\/B978-0-444-51624-4.50004-6"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Heath, Q., Miller, D.: A framework for proof certificates in finite state exploration. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings of the Fourth Workshop on Proof eXchange for Theorem Proving. Electronic Proceedings in Theoretical Computer Science, vol. 186, pp. 11\u201326. Open Publishing Association, August 2015","DOI":"10.4204\/EPTCS.186.0"},{"issue":"46","key":"16_CR29","doi-asserted-by":"publisher","first-page":"4747","DOI":"10.1016\/j.tcs.2009.07.041","volume":"410","author":"C Liang","year":"2009","unstructured":"Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theor. Comput. Sci. 410(46), 4747\u20134768 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"Libal, T., Volpe, M.: Certification of prefixed tableau proofs for modal logic. In: The Seventh International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2016). EPTCS, vol. 226, Catania, Italy, pp. 257\u2013271, September 2016","DOI":"10.4204\/EPTCS.226.18"},{"key":"16_CR31","unstructured":"Marin, S., Miller, D., Volpe, M.: A focused framework for emulating modal proof systems. In: Beklemishev, L., Demri, S., M\u00e1t\u00e9, A. (eds.) 11th Conference on Advances in Modal Logic. Advances in Modal Logic, vol. 11, Budapest, Hungary, pp. 469\u2013488. College Publications, August 2016"},{"key":"16_CR32","unstructured":"McCune, W.: Prover9 and mace4 (2010). http:\/\/www.cs.unm.edu\/~mccune\/prover9\/"},{"issue":"4","key":"16_CR33","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0747-7171(92)90011-R","volume":"14","author":"D Miller","year":"1992","unstructured":"Miller, D.: Unification under a mixed prefix. J. Symbolic Comput. 14(4), 321\u2013358 (1992)","journal-title":"J. Symbolic Comput."},{"key":"16_CR34","doi-asserted-by":"crossref","unstructured":"Miller, D.: Formalizing operational semantic specifications in logic. In: Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008), vol. 246, pp. 147\u2013165, August 2009","DOI":"10.1016\/j.entcs.2009.07.020"},{"issue":"3","key":"16_CR35","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/s00165-016-0393-z","volume":"29","author":"D Miller","year":"2017","unstructured":"Miller, D.: Proof checking and logic programming. Formal Aspects Comput. 29(3), 383\u2013399 (2017)","journal-title":"Formal Aspects Comput."},{"key":"16_CR36","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326","volume-title":"Programming with Higher-Order Logic","author":"D Miller","year":"2012","unstructured":"Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press, Cambridge (2012)"},{"key":"16_CR37","series-title":"Lecture Notes in Computer Science","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)","author":"D Miller","year":"2015","unstructured":"Miller, D., Volpe, M.: Focused labeled proof systems for modal logic. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). LNCS, vol. 9450. Springer, Heidelberg (2015)"},{"key":"16_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-0-387-34768-4_22","volume-title":"7th International Conference on Automated Deduction","author":"DA Miller","year":"1984","unstructured":"Miller, D.A.: Expansion tree proofs and their conversion to natural deduction proofs. In: Shostak, R.E. (ed.) CADE 1984. LNCS, vol. 170, pp. 375\u2013393. Springer, New York (1984). doi: 10.1007\/978-0-387-34768-4_22"},{"key":"16_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/3-540-48660-7_25","volume-title":"Automated Deduction \u2014 CADE-16","author":"G Nadathur","year":"1999","unstructured":"Nadathur, G., Mitchell, D.J.: System description: Teyjus\u2014a compiler and abstract machine based implementation of $$\\lambda $$ Prolog. In: Ganzinger, H. (ed.) CADE 1999. LNCS, vol. 1632, pp. 287\u2013291. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48660-7_25"},{"key":"16_CR40","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: Conference Record of the 24th Symposium on Principles of Programming Languages 1997, Paris, France, pp. 106\u2013119. ACM Press (1997)","DOI":"10.1145\/263699.263712"},{"key":"16_CR41","doi-asserted-by":"crossref","unstructured":"Pfenning, F.: Elf: a language for logic definition and verified metaprogramming. In: 4th International Symposium on Logic in Computer Science, Monterey, CA, pp. 313\u2013321, June 1989","DOI":"10.1109\/LICS.1989.39186"},{"key":"16_CR42","doi-asserted-by":"crossref","unstructured":"Pfenning, F.: Logic programming in the LF logical framework. In: Huet, G., Plotkin, G.D. (eds.) Logical Frameworks, pp. 149\u2013181. Cambridge University Press (1991)","DOI":"10.1017\/CBO9780511569807.008"},{"key":"16_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-14203-1_2","volume-title":"Automated Reasoning","author":"B Pientka","year":"2010","unstructured":"Pientka, B., Dunfield, J.: Beluga: a framework for programming and reasoning with deductive systems (system description). In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 15\u201321. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14203-1_2"},{"key":"16_CR44","first-page":"17","volume":"60\u201361","author":"GD Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. J. Logic Algebraic Program. 60\u201361, 17\u2013139 (2004)","journal-title":"J. Logic Algebraic Program."},{"key":"16_CR45","doi-asserted-by":"crossref","unstructured":"Pollack, R.: How to believe a machine-checked proof. In: Sambin, G., Smith, J. (eds.) Twenty Five Years of Constructive Type Theory. Oxford University Press (1998)","DOI":"10.7146\/brics.v4i18.18945"},{"key":"16_CR46","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12, 23\u201341 (1965)","journal-title":"J. ACM"},{"issue":"1\u20132","key":"16_CR47","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0743-1066(95)00035-I","volume":"24","author":"SM Shieber","year":"1995","unstructured":"Shieber, S.M., Schabes, Y., Pereira, F.C.N.: Principles and implementation of deductive parsing. J. Logic Program. 24(1\u20132), 3\u201336 (1995)","journal-title":"J. Logic Program."},{"issue":"1","key":"16_CR48","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s10703-012-0163-3","volume":"42","author":"A Stump","year":"2013","unstructured":"Stump, A., Oe, D., Reynolds, A., Hadarean, L., Tinelli, C.: SMT proof checking using a logical framework. Formal Methods Syst. Des. 42(1), 91\u2013118 (2013)","journal-title":"Formal Methods Syst. Des."},{"issue":"4","key":"16_CR49","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reasoning 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"16_CR50","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"AS Troelstra","year":"2000","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge University Press, Cambridge (2000)","edition":"2"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T19:24:43Z","timestamp":1750533883000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"11 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Gothenburg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 August 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 August 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.cade-26.info\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}