{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,17]],"date-time":"2026-01-17T20:00:21Z","timestamp":1768680021419,"version":"3.49.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031479625","type":"print"},{"value":"9783031479632","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[[2023]]},"DOI":"10.1007\/978-3-031-47963-2_8","type":"book-chapter","created":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T21:41:26Z","timestamp":1700689286000},"page":"100-118","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Towards the\u00a0Complexity Analysis of\u00a0Programming Language Proof Methods"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0162-9997","authenticated-orcid":false,"given":"Matteo","family":"Cimini","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,11,23]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Dal Lago, U., Vanoni, G.: The (in)efficiency of interaction. Proc. ACM Program. Lang. (PACMPL) 5(POPL), 1\u201333 (2021). https:\/\/doi.org\/10.1145\/3434332","DOI":"10.1145\/3434332"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/3-540-48168-0_32","volume-title":"Computer Science Logic","author":"T Altenkirch","year":"1999","unstructured":"Altenkirch, T., Reus, B.: Monadic presentations of lambda terms using generalized inductive types. In: Flum, J., Rodriguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 453\u2013468. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48168-0_32"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Bach Poulsen, C., Rouvoet, A., Tolmach, A., Krebbers, R., Visser, E.: Intrinsically-typed definitional interpreters for imperative languages. Proc. ACM Programm. Lang. (PACMPL) 2(POPL), 1\u201334 (2017). https:\/\/doi.org\/10.1145\/3158104","DOI":"10.1145\/3158104"},{"issue":"2","key":"8_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.6092\/issn.1972-5787\/4650","volume":"7","author":"D Baelde","year":"2014","unstructured":"Baelde, D., et al.: Abella: a system for reasoning about relational specifications. J. Formalized Reason. 7(2), 1\u201389 (2014). https:\/\/doi.org\/10.6092\/issn.1972-5787\/4650","journal-title":"J. Formalized Reason."},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Bellantoni, S.J., Cook, S.A.: A new recursion-theoretic characterization of the polytime functions (extended abstract). In: Proceedings of the Twenty-Fourth Annual ACM Symposium on Theory of Computing, pp. 283\u2013293. STOC 1992, Association for Computing Machinery, New York, NY, USA (1992). https:\/\/doi.org\/10.1145\/129712.129740","DOI":"10.1145\/129712.129740"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Cheney, J.: Toward a general theory of names: binding and scope. In: Pollack, R. (ed.) Proceedings of the 3rd ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding, pp. 33\u201340. MERLIN 2005, Association for Computing Machinery, New York, NY, USA (2005). https:\/\/doi.org\/10.1145\/1088454.1088459","DOI":"10.1145\/1088454.1088459"},{"key":"8_CR7","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5, 56\u201368 (1940). https:\/\/doi.org\/10.2307\/2266170","journal-title":"J. Symb. Log."},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Cimini, M.: Lang-n-prove: a DSL for language proofs. In: Proceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering, pp. 16\u201329. SLE 2022, Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3567512.3567514","DOI":"10.1145\/3567512.3567514"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-031-17108-6_4","volume-title":"Software Engineering and Formal Methods","author":"M Cimini","year":"2022","unstructured":"Cimini, M.: A query language for language analysis. In: Schlingloff, B.H., Chai, M. (eds.) SEFM 2022. LNCS, vol. 13550, pp. 57\u201373. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17108-6_4"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Cimini, M., Miller, D., Siek, J.G.: Extrinsically typed operational semantics for functional languages. In: L\u00e4mmel, R., Tratt, L., de Lara, J. (eds.) Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2020, Virtual Event, USA, 16\u201317 November 2020, pp. 108\u2013125. ACM (2020). https:\/\/doi.org\/10.1145\/3426425.3426936","DOI":"10.1145\/3426425.3426936"},{"key":"8_CR11","volume-title":"Frege: Philosophy of Language","author":"M Dummett","year":"1993","unstructured":"Dummett, M.: Frege: Philosophy of Language, 2nd edn. Harvard University Press, Cambridge (1993)","edition":"2"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Grewe, S., Erdweg, S., Wittmann, P., Mezini, M.: Type systems for the masses: deriving soundness proofs and efficient checkers. In: Murphy, G.C., Steele Jr., G.L. (eds.) 2015 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), pp. 137\u2013150. Onward! 2015, ACM, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2814228.2814239","DOI":"10.1145\/2814228.2814239"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Harper, R.: Practical Foundations for Programming Languages. 2 edn. Cambridge University Press, Cambridge (2016). https:\/\/doi.org\/10.1017\/CBO9781316576892","DOI":"10.1017\/CBO9781316576892"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Harper, R., Stone, C.: A type-theoretic interpretation of standard ML. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction: Essays in Honor of Robin Milner. MIT Press (2000). https:\/\/doi.org\/10.5555\/345868.345906","DOI":"10.5555\/345868.345906"},{"issue":"1\u20132","key":"8_CR15","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/S0304-3975(98)00357-0","volume":"228","author":"ND Jones","year":"1999","unstructured":"Jones, N.D.: LOGSPACE and PTIME characterized by programming languages. Theor. Comput. Sci. 228(1\u20132), 151\u2013174 (1999). https:\/\/doi.org\/10.1016\/S0304-3975(98)00357-0","journal-title":"Theor. Comput. Sci."},{"key":"8_CR16","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102440","volume":"194","author":"W Kokke","year":"2020","unstructured":"Kokke, W., Siek, J.G., Wadler, P.: Programming language foundations in Agda. Sci. Comput. Program. 194, 102440 (2020). https:\/\/doi.org\/10.1016\/j.scico.2020.102440","journal-title":"Sci. Comput. Program."},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/BFb0037112","volume-title":"Typed Lambda Calculi and Applications","author":"D Leivant","year":"1993","unstructured":"Leivant, D., Marion, J.-Y.: Lambda calculus characterizations of poly-time. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 274\u2013288. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/BFb0037112"},{"issue":"3","key":"8_CR18","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R Milner","year":"1978","unstructured":"Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17(3), 348\u2013375 (1978). https:\/\/doi.org\/10.1016\/0022-0000(78)90014-4","journal-title":"J. Comput. Syst. Sci."},{"key":"8_CR19","unstructured":"Pfenning, F.: Lecture notes on harmony (lecture 3) 15\u2013317: constructive logic (2009). https:\/\/www.cs.cmu.edu\/~fp\/courses\/15317-f09\/lectures\/03-harmony.pdf"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction \u2014 CADE-16","author":"F Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf \u2014 a meta-logical framework for deductive systems. In: CADE 1999. LNCS (LNAI), vol. 1632, pp. 202\u2013206. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48660-7_14"},{"key":"8_CR21","volume-title":"Types and Programming Languages","author":"BC Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Pottier, F., Simonet, V.: Information flow inference for ML. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 319\u2013330. POPL 2002, Association for Computing Machinery, New York, NY, USA (2002). https:\/\/doi.org\/10.1145\/503272.503302","DOI":"10.1145\/503272.503302"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"van der Rest, C., Poulsen, C.B., Rouvoet, A., Visser, E., Mosses, P.: Intrinsically-typed definitional interpreters \u00e0 la carte. Proc. ACM Program. Lang. (PACMPL) 6(OOPSLA2), 1903\u20131932 (2022). https:\/\/doi.org\/10.1145\/3563355","DOI":"10.1145\/3563355"},{"issue":"2","key":"8_CR24","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"WW Tait","year":"1967","unstructured":"Tait, W.W.: Intensional interpretations of functionals of finite type I. J. Symb. Log. 32(2), 198\u2013212 (1967). https:\/\/doi.org\/10.2307\/2271658","journal-title":"J. Symb. Log."},{"key":"8_CR25","doi-asserted-by":"publisher","unstructured":"Thiemann, P.: Intrinsically-typed mechanized semantics for session types. In: Komendantskaya, E. (ed.) Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, pp. 19:1\u201319:15. PPDP 2019, Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3354166.3354184","DOI":"10.1145\/3354166.3354184"},{"key":"8_CR26","doi-asserted-by":"publisher","unstructured":"Volpano, D., Irvine, C., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2\u20133), 167\u2013187 (1996). https:\/\/doi.org\/10.3233\/JCS-1996-42-304","DOI":"10.3233\/JCS-1996-42-304"},{"issue":"1","key":"8_CR27","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"AK Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38\u201394 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1093","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2023"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-47963-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T21:42:06Z","timestamp":1700689326000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-47963-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031479625","9783031479632"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-47963-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"23 November 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lima","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Peru","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 December 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 December 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2023.compsust.utec.edu.pe\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}