{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:13:12Z","timestamp":1767928392162,"version":"3.49.0"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030336356","type":"print"},{"value":"9783030336363","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-33636-3_12","type":"book-chapter","created":{"date-parts":[[2019,10,19]],"date-time":"2019-10-19T10:02:20Z","timestamp":1571479340000},"page":"329-365","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Shallow Embedding of Type Theory is Morally Correct"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9897-8936","authenticated-orcid":false,"given":"Ambrus","family":"Kaposi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6375-9781","authenticated-orcid":false,"given":"Andr\u00e1s","family":"Kov\u00e1cs","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8729-4077","authenticated-orcid":false,"given":"Nicolai","family":"Kraus","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,10,20]]},"reference":[{"issue":"POPL","key":"12_CR1","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/3158111","volume":"2","author":"A Abel","year":"2017","unstructured":"Abel, A., \u00d6hman, J., Vezzosi, A.: Decidability of conversion for type theory in type theory. Proc. ACM Program. Lang. 2(POPL), 23 (2017)","journal-title":"Proc. ACM Program. Lang."},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-319-89366-2_16","volume-title":"Foundations of Software Science and Computation Structures","author":"T Altenkirch","year":"2018","unstructured":"Altenkirch, T., Capriotti, P., Dijkstra, G., Kraus, N., Nordvall Forsberg, F.: Quotient inductive-inductive types. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 293\u2013310. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-89366-2_16"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Altenkirch, T., Kaposi, A.: Type theory in type theory using quotient inductive types. In: Bodik, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, 20\u201322 January 2016, St. Petersburg, FL, USA, pp. 18\u201329. ACM (2016). \n                    https:\/\/doi.org\/10.1145\/2837614.2837638","DOI":"10.1145\/2837614.2837638"},{"key":"12_CR4","doi-asserted-by":"publisher","unstructured":"Altenkirch, T., Kaposi, A.: Normalisation by evaluation for type theory, in type theory. Logical Methods Comput. Sci. 13(4) (2017). \n                    https:\/\/doi.org\/10.23638\/LMCS-13(4:1)2017","DOI":"10.23638\/LMCS-13(4:1)2017"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-94821-8_2","volume-title":"Interactive Theorem Proving","author":"A Anand","year":"2018","unstructured":"Anand, A., Boulier, S., Cohen, C., Sozeau, M., Tabareau, N.: Towards certified meta-programming with typed template-coq. In: Avigad, J., Mahboubi, A. (eds.) ITP 2018. LNCS, vol. 10895, pp. 20\u201339. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-94821-8_2"},{"issue":"02","key":"12_CR6","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1017\/S0956796812000056","volume":"22","author":"JP Bernardy","year":"2012","unstructured":"Bernardy, J.P., Jansson, P., Paterson, R.: Proofs for free \u2013 parametricity for dependent types. J. Funct. Program. 22(02), 107\u2013152 (2012). \n                    https:\/\/doi.org\/10.1017\/S0956796812000056","journal-title":"J. Funct. Program."},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Mogelberg, R.E., Schwinghammer, J., Stovring, K.: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. In: 2011 IEEE 26th Annual Symposium on Logic in Computer Science, pp. 55\u201364. IEEE (2011)","DOI":"10.1109\/LICS.2011.16"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Boulier, S., P\u00e9drot, P.M., Tabareau, N.: The next 700 syntactical models of type theory. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp. 182\u2013194. ACM, New York (2017). \n                    https:\/\/doi.org\/10.1145\/3018610.3018620","DOI":"10.1145\/3018610.3018620"},{"issue":"5","key":"12_CR9","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1017\/S095679681300018X","volume":"23","author":"E Brady","year":"2013","unstructured":"Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23(5), 552\u2013593 (2013)","journal-title":"J. Funct. Program."},{"key":"12_CR10","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.entcs.2008.12.114","volume":"228","author":"J Chapman","year":"2009","unstructured":"Chapman, J.: Type theory should eat itself. Electron. Notes Theor. Comput. Sci. 228, 21\u201336 (2009). \n                    https:\/\/doi.org\/10.1016\/j.entcs.2008.12.114","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008, pp. 143\u2013156. ACM, New York (2008). \n                    https:\/\/doi.org\/10.1145\/1411204.1411226","DOI":"10.1145\/1411204.1411226"},{"key":"12_CR12","unstructured":"Cockx, J., Abel, A.: Sprinkles of extensionality for your vanilla type theory. In: TYPES 2016 (2016)"},{"key":"12_CR13","unstructured":"Cohen, C., Coquand, T., Huber, S., M\u00f6rtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom, December 2015"},{"key":"12_CR14","unstructured":"Coquand, T.: Canonicity and normalisation for dependent type theory. CoRR (2018). \n                    http:\/\/arxiv.org\/abs\/1810.09367"},{"key":"12_CR15","unstructured":"Coquand, T., Huber, S., Sattler, C.: Homotopy canonicity for cubical type theory. In: Geuvers, H. (ed.) Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) (2019)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-74464-1_7","volume-title":"Types for Proofs and Programs","author":"NA Danielsson","year":"2007","unstructured":"Danielsson, N.A.: A formalisation of a dependently typed language as an inductive-recursive family. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 93\u2013109. Springer, Heidelberg (2007). \n                    https:\/\/doi.org\/10.1007\/978-3-540-74464-1_7"},{"key":"12_CR17","first-page":"124","volume-title":"Lecture Notes in Computer Science","author":"Jo\u00eblle Despeyroux","year":"1995","unstructured":"Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-Order Abstract Syntax in Coq. Technical Report RR-2556, INRIA, May 1995. \n                    https:\/\/hal.inria.fr\/inria-00074124"},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Devriese, D., Piessens, F.: Typed syntactic meta-programming. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming (ICFP 2013). pp. 73\u201385. ACM, September 2013. \n                    https:\/\/doi.org\/10.1145\/2500365.2500575","DOI":"10.1145\/2500365.2500575"},{"key":"12_CR19","unstructured":"Diehl, L.: Fully Generic Programming over Closed Universes of Inductive-Recursive Types. Ph.D. thesis, Portland State University (2017)"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/3-540-61780-9_66","volume-title":"Types for Proofs and Programs","author":"P Dybjer","year":"1996","unstructured":"Dybjer, P.: Internal type theory. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 120\u2013134. Springer, Heidelberg (1996). \n                    https:\/\/doi.org\/10.1007\/3-540-61780-9_66"},{"key":"12_CR21","unstructured":"Hofmann, M.: Extensional concepts in intensional type theory. Thesis, University of Edinburgh, Department of Computer Science (1995)"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: Syntax and semantics of dependent types. In: Semantics and Logics of Computation, pp. 79\u2013130. Cambridge University Press (1997)","DOI":"10.1017\/CBO9780511526619.004"},{"key":"12_CR23","unstructured":"Hofmann, M.: Semantical analysis of higher-order abstract syntax. In: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, LICS 1999, p. 204. IEEE Computer Society, Washington (1999). \n                    http:\/\/dl.acm.org\/citation.cfm?id=788021.788940"},{"key":"12_CR24","doi-asserted-by":"publisher","unstructured":"Hou (Favonia), K.B., Finster, E., Licata, D.R., Lumsdaine, P.L.: A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2016, pp. 565\u2013574. ACM, New York (2016). \n                    https:\/\/doi.org\/10.1145\/2933575.2934545","DOI":"10.1145\/2933575.2934545"},{"key":"12_CR25","unstructured":"Huber, S.: Cubical Interpretations of Type Theory. Ph.D. thesis, University of Gothenburg (2016)"},{"key":"12_CR26","doi-asserted-by":"publisher","unstructured":"Jaber, G., Lewertowski, G., P\u00e9drot, P.M., Sozeau, M., Tabareau, N.: The definitional side of the forcing. In: Logics in Computer Science, New York, United States, May 2016. \n                    https:\/\/doi.org\/10.1145\/2933575.2935320","DOI":"10.1145\/2933575.2935320"},{"key":"12_CR27","unstructured":"Kaposi, A., Huber, S., Sattler, C.: Gluing for type theory. In: Geuvers, H. (ed.) Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) (2019)"},{"key":"12_CR28","doi-asserted-by":"publisher","unstructured":"Kaposi, A., Kov\u00e1cs, A.: A syntax for higher inductive-inductive types. In: Kirchner, H. (ed.) 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), vol. 108, pp. 20:1\u201320:18. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2018). \n                    https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2018.20","DOI":"10.4230\/LIPIcs.FSCD.2018.20"},{"issue":"POPL","key":"12_CR29","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/3290315","volume":"3","author":"A Kaposi","year":"2019","unstructured":"Kaposi, A., Kov\u00e1cs, A., Altenkirch, T.: Constructing quotient inductive-inductive types. Proc. ACM Program. Lang. 3(POPL), 2 (2019)","journal-title":"Proc. ACM Program. Lang."},{"key":"12_CR30","unstructured":"Kaposi, A., Kov\u00e1cs, A., Kraus, N.: Formalisations in Agda using a morally correct shallow embedding, May 2019. \n                    https:\/\/bitbucket.org\/akaposi\/shallow\/src\/master\/"},{"key":"12_CR31","unstructured":"Licata, D.: Running circles around (in) your proof assistant; or, quotients that compute (2011). \n                    http:\/\/homotopytypetheory.org\/2011\/04\/23\/running-circles-around-in-your-proof-assistant\/"},{"key":"12_CR32","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/S0049-237X(08)71945-1","volume-title":"Logic Colloquium '73, Proceedings of the Logic Colloquium","author":"Per Martin-L\u00f6f","year":"1975","unstructured":"Martin-L\u00f6f, P.: An intuitionistic theory of types: predicative part. In: Rose, H., Shepherdson, J. (eds.) Logic Colloquium \u201973, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics, North-Holland, vol. 80, pp. 73\u2013118 (1975)"},{"key":"12_CR33","unstructured":"The Coq development team: The Coq proof assistant reference manual. LogiCal Project (2019). \n                    http:\/\/coq.inria.fr\n                    \n                  . version 8.9"},{"key":"12_CR34","doi-asserted-by":"publisher","unstructured":"McBride, C.: Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation. In: Oliveira, B.C.d.S., Zalewski, M. (eds.) Proceedings of the ACM SIGPLAN Workshop on Generic Programming, pp. 1\u201312. ACM (2010). \n                    https:\/\/doi.org\/10.1145\/1863495.1863497","DOI":"10.1145\/1863495.1863497"},{"key":"12_CR35","doi-asserted-by":"publisher","unstructured":"McBride, C., McKinna, J.: Functional pearl: I am not a number \u2013 I am a free variable. In: Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell, Haskell 2004, pp. 1\u20139. ACM, New York (2004). \n                    https:\/\/doi.org\/10.1145\/1017472.1017477\n                    \n                  . \n                    http:\/\/doi.acm.org\/10.1145\/1017472.1017477","DOI":"10.1145\/1017472.1017477"},{"key":"12_CR36","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction - CADE-25","author":"L Moura de","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). \n                    https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"12_CR37","unstructured":"Nordvall Forsberg, F.: Inductive-inductive definitions. Ph.D. thesis, Swansea University (2013)"},{"key":"12_CR38","doi-asserted-by":"publisher","unstructured":"Orton, I., Pitts, A.M.: Axioms for modelling cubical type theory in a topos. In: Talbot, J.M., Regnier, L. (eds.) 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), vol. 62, pp. 24:1\u201324:19. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2016). \n                    https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2016.24","DOI":"10.4230\/LIPIcs.CSL.2016.24"},{"issue":"7","key":"12_CR39","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1145\/960116.54010","volume":"23","author":"F Pfenning","year":"1988","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. SIGPLAN Not. 23(7), 199\u2013208 (1988). \n                    https:\/\/doi.org\/10.1145\/960116.54010","journal-title":"SIGPLAN Not."},{"key":"12_CR40","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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 (LNAI), vol. 6173, pp. 15\u201321. Springer, Heidelberg (2010). \n                    https:\/\/doi.org\/10.1007\/978-3-642-14203-1_2"},{"key":"12_CR41","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Mason, R.E.A. (ed.) Information Processing 1983, Proceedings of the IFIP 9th World Computer Congress, Paris, 19\u201323 September 1983, pp. 513\u2013523. Elsevier Science Publishers B. V. (North-Holland), Amsterdam (1983)"},{"issue":"ICFP","key":"12_CR42","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3236787","volume":"2","author":"Nicolas Tabareau","year":"2018","unstructured":"Tabareau, N., Tanter, \u00c9., Sozeau, M.: Equivalences for free. Proc. ACM Program. Lang. 1\u201329 (2018). \n                    https:\/\/hal.inria.fr\/hal-01559073","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"12_CR43","unstructured":"The Agda development team: Agda (2015). \n                    http:\/\/wiki.portal.chalmers.se\/agda"},{"key":"12_CR44","doi-asserted-by":"publisher","unstructured":"Wieczorek, P., Biernacki, D.: A Coq formalization of normalization by evaluation for Martin-L\u00f6f type theory. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pp. 266\u2013279. ACM, New York (2018). \n                    https:\/\/doi.org\/10.1145\/3167091","DOI":"10.1145\/3167091"},{"key":"12_CR45","doi-asserted-by":"crossref","unstructured":"Winterhalter, T., Sozeau, M., Tabareau, N.: Eliminating reflection from type theory. In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 91\u2013103. ACM (2019)","DOI":"10.1145\/3293880.3294095"}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-33636-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,19]],"date-time":"2019-10-19T10:10:51Z","timestamp":1571479851000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-33636-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030336356","9783030336363"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-33636-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"20 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"MPC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Mathematics of Program Construction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mpc2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.nott.ac.uk\/~pszgmh\/mpc19.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"68% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}