{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:42:40Z","timestamp":1767926560352,"version":"3.49.0"},"publisher-location":"Singapore","reference-count":55,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819789429","type":"print"},{"value":"9789819789436","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-981-97-8943-6_4","type":"book-chapter","created":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T08:45:29Z","timestamp":1730105129000},"page":"63-83","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-2216-8830","authenticated-orcid":false,"given":"Bohdan","family":"Liesnikov","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3862-4073","authenticated-orcid":false,"given":"Jesper","family":"Cockx","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,28]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","unstructured":"Abel, A., Chapman, J.: Normalization by evaluation in the delay monad: a case study for conduction via copatterns and sized types (2014). https:\/\/doi.org\/10.4204\/EPTCS.153.4","DOI":"10.4204\/EPTCS.153.4"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Abel, A., \u00d6hman, J., Vezzosi, A.: Decidability of conversion for type theory in type theory. In: Proceedings of the ACM on Programming Languages 2(POPL), 23:1\u201323:29 (2017). https:\/\/doi.org\/10.1145\/3158111","DOI":"10.1145\/3158111"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Adams, R.: Formalized metatheory with terms represented by an indexed family of types. In: Filli\u00e2tre, J.C., Paulin-Mohring, C., Werner, B. (eds.) Types for Proofs and Programs. pp. 1\u201316. Springer, Berlin, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11617990_1","DOI":"10.1007\/11617990_1"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Adjedj, A., Lennon-Bertrand, M., Maillard, K., P\u00e9drot, P.M., Pujet, L.: Martin-L\u00f6f \u00e0 la Coq. In: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs. pp. 230\u2013245. CPP 2024, Association for Computing Machinery, New York, NY, USA (2024).https:\/\/doi.org\/10.1145\/3636501.3636951","DOI":"10.1145\/3636501.3636951"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Altenkirch, T., Kaposi, A.: Type theory in type theory using quotient inductive types. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 18\u201329. ACM, St. Petersburg FL USA (2016). https:\/\/doi.org\/10.1145\/2837614.2837638","DOI":"10.1145\/2837614.2837638"},{"key":"4_CR6","unstructured":"Kaposi, A.: Towards quotient inductive-inductive-recursive types. In: 29th International Conference on Types for Proofs and Programs TYPES 2023 \u2013 Abstracts. pp. 124\u2013126. Valencia (Spain) (2023). https:\/\/types2023.webs.upv.es\/TYPES2023.pdf#section.11.4"},{"key":"4_CR7","doi-asserted-by":"publisher","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.) Interactive Theorem Proving, vol. 10895, pp. 20\u201339. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94821-8_2","DOI":"10.1007\/978-3-319-94821-8_2"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Appel, A.W., Michael, N., Stump, A., Virga, R.: A Trustworthy proof checker. J. Autom. Reason. 31(3), 231\u2013260 (2003). https:\/\/doi.org\/10.1023\/B:JARS.0000021013.61329.58","DOI":"10.1023\/B:JARS.0000021013.61329.58"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Atkey, R.: Syntax and semantics of quantitative type theory. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 56\u201365. LICS \u201918, Association for Computing Machinery, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3209108.3209189","DOI":"10.1145\/3209108.3209189"},{"issue":"2","key":"4_CR10","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H Barendregt","year":"1991","unstructured":"Barendregt, H.: Introduction to generalized type systems. J. Funct. Program. 1(2), 125\u2013154 (1991). https:\/\/doi.org\/10.1017\/S0956796800020025","journal-title":"J. Funct. Program."},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"Bauer, A., Gilbert, G., Haselwarter, P.G., Pretnar, M., Stone, C.A.: Design and implementation of the andromeda proof assistant. In: DROPS-IDN\/v2\/Document\/10.4230\/LIPIcs.TYPES.2016.5. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2018). https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2016.5","DOI":"10.4230\/LIPIcs.TYPES.2016.5"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Bird, R.S., Paterson, R.: De Bruijn notation as a nested datatype. J. Funct. Program. 9(1), 77\u201391 (1999). https:\/\/doi.org\/10.1017\/S0956796899003366","DOI":"10.1017\/S0956796899003366"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Bodin, M., Chargueraud, A., Filaretti, D., Gardner, P., Maffeis, S., Naudziuniene, D., Schmitt, A., Smith, G.: A trusted mechanised JavaScript specification. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 87\u2013100. POPL \u201914, Association for Computing Machinery, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2535838.2535876","DOI":"10.1145\/2535838.2535876"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23(5), 552\u2013593 (2013). https:\/\/doi.org\/10.1017\/S095679681300018X","DOI":"10.1017\/S095679681300018X"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Bruijnde Bruijn, N.G.: The mathematical language AUTOMATH, its usage, and some of its extensions. In: Laudet, M., Lacombe, D., Nolin, L., Sch\u00fctzenberger, M. (eds.) Symposium on Automatic Demonstration. pp. 29\u201361. Springer, Berlin, Heidelberg (1970). https:\/\/doi.org\/10.1007\/BFb0060623","DOI":"10.1007\/BFb0060623"},{"key":"4_CR16","unstructured":"Barras, B.: Coq en coq. Rapport de Recherche\u00a03026, INRIA (1996)"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Carneiro, M.: Lean4Lean: towards a formalized metatheory for the Lean theorem prover (2024). https:\/\/doi.org\/10.48550\/arXiv.2403.14064","DOI":"10.48550\/arXiv.2403.14064"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Cauderlier, R., Dubois, C.: FoCaLiZe and dedukti to the rescue for proof interoperability. In: Itp, pp. 131\u2013147 (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_9","DOI":"10.1007\/978-3-319-66107-0_9"},{"key":"4_CR19","doi-asserted-by":"publisher","unstructured":"Chapman, J.: Type Theory should eat itself. Electron. Notes Theor. Comput. Sci. 228, 21\u201336 (2009). https:\/\/doi.org\/10.1016\/j.entcs.2008.12.114","DOI":"10.1016\/j.entcs.2008.12.114"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Coquand, T.: An algorithm for testing conversion in type theory. In: Logical Frameworks, pp. 255\u2013279. Cambridge University Press, USA (1991)","DOI":"10.1017\/CBO9780511569807.011"},{"key":"4_CR21","doi-asserted-by":"publisher","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76(2), 95\u2013120 (1988). https:\/\/doi.org\/10.1016\/0890-5401(88)90005-3","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Curien, P.L.: An abstract framework for environment machines. Theor. Comput. Sci. 82(2), 389\u2013402 (1991). https:\/\/doi.org\/10.1016\/0304-3975(91)90230-Y","DOI":"10.1016\/0304-3975(91)90230-Y"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Danielsson, N.A.: Operational semantics using the partiality monad. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming. pp. 127\u2013138. ICFP \u201912. Association for Computing Machinery, New York, NY, USA (2012). https:\/\/doi.org\/10.1145\/2364527.2364546","DOI":"10.1145\/2364527.2364546"},{"key":"4_CR24","unstructured":"Danielsson, N.A.: Logical properties of a modality for erasure (2019). https:\/\/www.cse.chalmers.se\/~nad\/publications\/danielsson-erased.pdf"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Devriese, D., Piessens, F.: Typed syntactic meta-programming. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming - ICFP \u201913, p.\u00a073. ACM Press, Boston, Massachusetts, USA (2013). https:\/\/doi.org\/10.1145\/2500365.2500575","DOI":"10.1145\/2500365.2500575"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"Dunfield, J., Krishnaswami, N.: Bidirectional typing. ACM Comput. Surveys 54(5), 98:1\u201398:38 (2021). https:\/\/doi.org\/10.1145\/3450952","DOI":"10.1145\/3450952"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Eisenberg, R.A.: Stitch: The sound type-indexed type checker (functional pearl). In: Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell, pp. 39\u201353. Haskell 2020. Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3406088.3409015","DOI":"10.1145\/3406088.3409015"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF. Lecture Notes in Computer Science, vol. 78. Springer, Berlin, Heidelberg (1979)","DOI":"10.1007\/3-540-09724-4"},{"key":"4_CR29","unstructured":"Jesper Cockx: Operations on syntax should not inspect the scope. In: Reyes, E.H., Villanueva, A. (eds.) TYPES 2023 \u2013 Abstracts, pp. 138\u2013140. Valencia, Spain (2023). https:\/\/types2023.webs.upv.es\/TYPES2023.pdf"},{"key":"4_CR30","doi-asserted-by":"publisher","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, pp. 207\u2013220. SOSP \u201909, Association for Computing Machinery, New York, NY, USA (2009). https:\/\/doi.org\/10.1145\/1629575.1629596","DOI":"10.1145\/1629575.1629596"},{"key":"4_CR31","doi-asserted-by":"publisher","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: A verified implementation of ML. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 179\u2013191. POPL\u201914, Association for Computing Machinery, New York, NY, USA (Jan 2014) https:\/\/doi.org\/10.1145\/2535838.2535841","DOI":"10.1145\/2535838.2535841"},{"key":"4_CR32","unstructured":"Paulson, L.C.: Isabelle: the next 700 theorem provers. In: P. Odifreddi (ed.) Logic and Computer Science, pp. 361\u2013386. A.P.I.C. Studies in Data Processing, Academic Press (1990). https:\/\/www.cl.cam.ac.uk\/~lp15\/papers\/Isabelle\/chap700.pdf"},{"issue":"7","key":"4_CR33","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","journal-title":"Commun. ACM"},{"key":"4_CR34","unstructured":"Malecha, G.: Extensible proof engineering in intensional type theory. Ph.D. thesis, Harvard University, Graduate School of Arts & Sciences., Cambridge, Massachusetts (2014). http:\/\/nrs.harvard.edu\/urn-3:HUL.InstRepos:17467172"},{"key":"4_CR35","doi-asserted-by":"publisher","unstructured":"McBride, C.: Elimination with a motive. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R., Pollack, R. (eds.) Types for Proofs and Programs, pp. 197\u2013216. Springer, Berlin, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45842-5_13","DOI":"10.1007\/3-540-45842-5_13"},{"key":"4_CR36","doi-asserted-by":"publisher","unstructured":"McBride, C.: I Got Plenty o\u2019 Nuttin\u2019. In: Lindley, S., McBride, C., Trinder, P., Sannella, D. (eds.) A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, pp. 207\u2013233. Lecture Notes in Computer Science. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30936-1_12","DOI":"10.1007\/978-3-319-30936-1_12"},{"key":"4_CR37","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C., Goos, G., Hartmanis, J., Van\u00a0Leeuwen, J. (eds.): Isabelle\/HOL, Lecture Notes in Computer Science, vol.\u00a02283. Springer, Berlin, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"4_CR38","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Chalmers University of Technology and G\u00f6teborg University, G\u00f6teborg, Sweden (2007). https:\/\/www.cse.chalmers.se\/~ulfn\/papers\/thesis.pdf"},{"key":"4_CR39","doi-asserted-by":"publisher","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf\u2014A meta-logical framework for deductive systems, vol.\u00a01632, pp. 202\u2013206. Springer, Berlin, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48660-7_14","DOI":"10.1007\/3-540-48660-7_14"},{"key":"4_CR40","doi-asserted-by":"publisher","unstructured":"Pierce, B.C., Turner, D.N.: Local type inference. ACM Trans. Program. Lang. Syst. 22(1), 1\u201344 (2000). https:\/\/doi.org\/10.1145\/345099.345100","DOI":"10.1145\/345099.345100"},{"key":"4_CR41","doi-asserted-by":"publisher","unstructured":"Pollack, R.: How to believe a machine-checked proof. In: Sambin, G., Smith, J.M. (eds.) Twenty Five Years of Constructive Type Theory, p.\u00a00. Oxford University Press (Oct 1998). https:\/\/doi.org\/10.1093\/oso\/9780198501275.003.0013","DOI":"10.1093\/oso\/9780198501275.003.0013"},{"key":"4_CR42","doi-asserted-by":"publisher","unstructured":"Sch\u00e4fer, S., Tebbi, T., Smolka, G.: Autosubst: reasoning with de Bruijn terms and parallel substitutions. In: Urban, C., Zhang, X. (eds.) Interactive Theorem Proving. pp. 359\u2013374. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_24","DOI":"10.1007\/978-3-319-22102-1_24"},{"key":"4_CR43","doi-asserted-by":"publisher","unstructured":"Sestoft, P.: Deriving a lazy abstract machine. J. Funct. Program. 7(3), 231\u2013264 (1997). https:\/\/doi.org\/10.1017\/S0956796897002712","DOI":"10.1017\/S0956796897002712"},{"key":"4_CR44","doi-asserted-by":"publisher","unstructured":"Sozeau, M., Anand, A., Boulier, S., Cohen, C., Forster, Y., Kunze, F., Malecha, G., Tabareau, N., Winterhalter, T.: The MetaCoq Project. J. Autom. Reason. 64(5), 947\u2013999 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09540-0","DOI":"10.1007\/s10817-019-09540-0"},{"key":"4_CR45","doi-asserted-by":"publisher","unstructured":"Sozeau, M., Boulier, S., Forster, Y., Tabareau, N., Winterhalter, T.: Coq Coq correct! verification of type checking and erasure for Coq, in Coq. Proceedings of the ACM on Programming Languages 4(POPL), 1\u201328 (2020)https:\/\/doi.org\/10.1145\/3371076","DOI":"10.1145\/3371076"},{"key":"4_CR46","unstructured":"Sozeau, M., Forster, Y., Lennon-Bertrand, M., Nielsen, J.B., Tabareau, N., Winterhalter, T.: Correct and Complete Type Checking and Certified Erasure for Coq, in Coq (2023). https:\/\/inria.hal.science\/hal-04077552"},{"key":"4_CR47","doi-asserted-by":"publisher","unstructured":"Stark, K., Sch\u00e4fer, S., Kaiser, J.: Autosubst 2: Reasoning with multi-sorted de Bruijn terms and vector substitutions. In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 166\u2013180. CPP 2019. Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3293880.3294101","DOI":"10.1145\/3293880.3294101"},{"key":"4_CR48","doi-asserted-by":"publisher","unstructured":"Strub, P.Y., Swamy, N., Fournet, C., Chen, J.: Self-certification: Bootstrapping certified typecheckers in F* with Coq. ACM SIGPLAN Notices 47(1), 571\u2013584 (Jan2012). https:\/\/doi.org\/10.1145\/2103621.2103723","DOI":"10.1145\/2103621.2103723"},{"key":"4_CR49","doi-asserted-by":"publisher","unstructured":"Tan, Y.K., Owens, S., Kumar, R.: A verified type system for CakeML. In: Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages. pp. 1\u201312. IFL \u201915, Association for Computing Machinery, New York, NY, USA (2015).https:\/\/doi.org\/10.1145\/2897336.2897344","DOI":"10.1145\/2897336.2897344"},{"key":"4_CR50","unstructured":"The Agda Development Team: Agda 2.6.4 documentation (2023). https:\/\/agda.readthedocs.io\/en\/v2.6.4\/"},{"key":"4_CR51","unstructured":"The Coq Development Team: The coq reference manual \u2013 release 8.18.0 (2023). https:\/\/coq.inria.fr\/doc\/V8.18.0\/refman"},{"key":"4_CR52","unstructured":"The Idris Development Team: Documentation for the Idris language \u2013 version 1.3.4 (2020). http:\/\/docs.idris-lang.org\/en\/v1.3.4\/"},{"key":"4_CR53","doi-asserted-by":"publisher","unstructured":"Weirich, S., Voizard, A., amorimde Amorim, P.H.A., Eisenberg, R.A.: A specification for dependent types in Haskell. PACMPL 1(ICFP) (2017). https:\/\/doi.org\/10.1145\/3110275","DOI":"10.1145\/3110275"},{"key":"4_CR54","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, pp. 266\u2013279. CPP 2018. Association for Computing Machinery, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3167091","DOI":"10.1145\/3167091"},{"key":"4_CR55","doi-asserted-by":"publisher","unstructured":"Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.: Verdi: A framework for implementing and formally verifying distributed systems. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 357\u2013368. PLDI \u201915, Association for Computing Machinery, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2737924.2737958","DOI":"10.1145\/2737924.2737958"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-97-8943-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T16:52:45Z","timestamp":1748364765000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-97-8943-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,28]]},"ISBN":["9789819789429","9789819789436"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-981-97-8943-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,28]]},"assertion":[{"value":"28 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kyoto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}