{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,7]],"date-time":"2025-12-07T16:02:34Z","timestamp":1765123354347,"version":"3.41.0"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031669965"},{"type":"electronic","value":"9783031669972"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-66997-2_16","type":"book-chapter","created":{"date-parts":[[2024,8,3]],"date-time":"2024-08-03T20:03:12Z","timestamp":1722715392000},"page":"279-297","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Partial Proof Terms in\u00a0the\u00a0Study of\u00a0Idealized Proof Search"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6348-5653","authenticated-orcid":false,"given":"Jos\u00e9","family":"Esp\u00edrito Santo","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5352-4807","authenticated-orcid":false,"given":"Ana Catarina","family":"Sousa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,29]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Alves, S., Broda, S.: A short note on type-inhabitation: Formula-trees vs. game semantics. Inf. Process. Lett. 115(11), 908\u2013911 (2015)","DOI":"10.1016\/j.ipl.2015.05.004"},{"key":"16_CR2","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-642-21691-6_8","volume-title":"TLCA 2011","author":"P Bourreau","year":"2011","unstructured":"Bourreau, P., Salvati, S.: Game semantics and uniqueness of type inhabitance in the simply-typed $$\\lambda $$-calculus. In: Ong, L. (ed.) TLCA 2011. LNCS, vol. 6690, pp. 61\u201375. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21691-6_8"},{"issue":"5","key":"16_CR3","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1093\/logcom\/13.5.639","volume":"13","author":"I Cervesato","year":"2003","unstructured":"Cervesato, I., Pfenning, F.: A linear spine calculus. J. Log. Comput. 13(5), 639\u2013688 (2003)","journal-title":"J. Log. Comput."},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Dunfield, J., Krishnaswami, N.: Bidirectional typing. ACM Comput. Surv. 54(5), 98:1\u201398:38 (2022)","DOI":"10.1145\/3450952"},{"key":"16_CR5","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/11780342_19","volume-title":"CiE 2006","author":"R Dyckhoff","year":"2006","unstructured":"Dyckhoff, R., Lengrand, S.: LJQ, a strongly focused calculus for intuitionistic logic. In: Beckmann, A., Berger, U., L\u00f6we, B., Tucker, J.V. (eds.) CiE 2006. LNCS, vol. 3988, pp. 173\u2013185. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11780342_19"},{"issue":"1","key":"16_CR6","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1023\/A:1005099619660","volume":"60","author":"R Dyckhoff","year":"1998","unstructured":"Dyckhoff, R., Pinto, L.: Cut-elimination and a permutation-free sequent calculus for intuitionistic logic. Stud. Logica. 60(1), 107\u2013118 (1998)","journal-title":"Stud. Logica."},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Dyckhoff, R., Pinto, L.: Proof search in constructive logics. Lecture Notes of the London Mathematical Society, vol. 258, pp. 53\u201365 (1999)","DOI":"10.1017\/CBO9781107325944.004"},{"key":"16_CR8","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/3-540-36078-6_24","volume-title":"LPAR 2002","author":"J Esp\u00edrito Santo","year":"2002","unstructured":"Esp\u00edrito Santo, J.: An isomorphism between a fragment of sequent calculus and an extension of natural deduction. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS, vol. 2514, pp. 352\u2013366. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36078-6_24"},{"issue":"4","key":"16_CR9","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1007\/s00224-009-9183-9","volume":"45","author":"J Esp\u00edrito Santo","year":"2009","unstructured":"Esp\u00edrito Santo, J.: The lambda-calculus and the unity of structural proof theory. Theory Comput. Syst. 45(4), 963\u2013994 (2009)","journal-title":"Theory Comput. Syst."},{"issue":"6","key":"16_CR10","doi-asserted-by":"publisher","first-page":"618","DOI":"10.1016\/j.apal.2012.05.008","volume":"164","author":"J Esp\u00edrito Santo","year":"2013","unstructured":"Esp\u00edrito Santo, J.: Towards a canonical classical natural deduction system. Ann. Pure Appl. Log. 164(6), 618\u2013650 (2013)","journal-title":"Ann. Pure Appl. Log."},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Esp\u00edrito Santo, J.: The polarized $$\\lambda $$-calculus. In: Nigam, V., Florido, M. (eds.) 11th Workshop on Logical and Semantic Frameworks with Applications, LSFA 2016, Porto, Portugal, 1 January 2016. Electronic Notes in Theoretical Computer Science, vol.\u00a0332, pp. 149\u2013168. Elsevier (2016)","DOI":"10.1016\/j.entcs.2017.04.010"},{"issue":"1\u20133","key":"16_CR12","doi-asserted-by":"publisher","first-page":"111","DOI":"10.3233\/FI-2019-1857","volume":"170","author":"J Esp\u00edrito Santo","year":"2019","unstructured":"Esp\u00edrito Santo, J., Matthes, R., Pinto, L.: Decidability of several concepts of finiteness for simple types. Fundam. Inform. 170(1\u20133), 111\u2013138 (2019)","journal-title":"Fundam. Inform."},{"issue":"8","key":"16_CR13","doi-asserted-by":"publisher","first-page":"1092","DOI":"10.1017\/S0960129518000099","volume":"29","author":"J Esp\u00edrito Santo","year":"2019","unstructured":"Esp\u00edrito Santo, J., Matthes, R., Pinto, L.: Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search. Math. Struct. Comput. Sci. 29(8), 1092\u20131124 (2019)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"10","key":"16_CR14","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2021.103026","volume":"172","author":"J Esp\u00edrito Santo","year":"2021","unstructured":"Esp\u00edrito Santo, J., Matthes, R., Pinto, L.: A coinductive approach to proof search through typed lambda-calculi. Ann. Pure Appl. Logic 172(10), 103026 (2021)","journal-title":"Ann. Pure Appl. Logic"},{"key":"16_CR15","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/3-540-45793-3_36","volume-title":"CSL 2002","author":"H Geuvers","year":"2002","unstructured":"Geuvers, H., Jojgov, G.I.: Open proofs and open terms: a basis for interactive logic. In: Bradfield, J.C. (ed.) CSL 2002. LNCS, vol. 2471, pp. 537\u2013552. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45793-3_36"},{"key":"16_CR16","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/BFb0022247","volume-title":"CSL 1994","author":"H Herbelin","year":"1995","unstructured":"Herbelin, H.: A $$\\lambda $$-calculus structure isomorphic to a Gentzen-style sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 61\u201375. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/BFb0022247"},{"key":"16_CR17","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 logic. Theor. Comput. Sci. 410, 4747\u20134768 (2009)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20132","key":"16_CR18","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D Miller","year":"1991","unstructured":"Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Ann. Pure Appl. Log. 51(1\u20132), 125\u2013157 (1991)","journal-title":"Ann. Pure Appl. Log."},{"key":"16_CR19","unstructured":"Mints, G.: Selected Papers in Proof Theory. Bibliopolis (1992)"},{"key":"16_CR20","unstructured":"Mints, G.: A Short Introduction to Intuitionistic Logic. Kluwer Academic Publishers (2002)"},{"issue":"1","key":"16_CR21","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1017\/S0960129500003261","volume":"11","author":"CA Mu\u00f1oz","year":"2001","unstructured":"Mu\u00f1oz, C.A.: Dependent types and explicit substitutions: a meta-theoretical development. Math. Struct. Comput. Sci. 11(1), 91\u2013129 (2001)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1\u20132","key":"16_CR22","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1016\/S0304-3975(00)00196-1","volume":"266","author":"CA Mu\u00f1oz","year":"2001","unstructured":"Mu\u00f1oz, C.A.: Proof-term synthesis on dependent-type systems via explicit substitutions. Theor. Comput. Sci. 266(1\u20132), 407\u2013440 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. ACM Trans. Comput. Log. 9(3), 23:1\u201323:49 (2008)","DOI":"10.1145\/1352582.1352591"},{"key":"16_CR24","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2022.100827","volume":"130","author":"C Olarte","year":"2023","unstructured":"Olarte, C., Pimentel, E., Rocha, C.: A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems. J. Log. Algebraic Methods Program. 130, 100827 (2023)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"16_CR25","unstructured":"Prawitz, D.: Natural Deduction. A Proof-Theoretical Study. Almquist and Wiksell, Stockholm (1965)"},{"key":"16_CR26","unstructured":"Schubert, A., Dekkers, W., Barendregt, H.P.: Automata theoretic account of proof search. In: Kreutzer, S. (ed.) 24th EACSL Annual Conference on Computer Science Logic, CSL 2015. LIPIcs, vol.\u00a041, pp. 128\u2013143. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)"},{"issue":"1","key":"16_CR27","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1023\/A:1005091418752","volume":"60","author":"W Sieg","year":"1998","unstructured":"Sieg, W., Byrnes, J.: Normal natural deduction proofs (in classical logic). Stud. Logica. 60(1), 67\u2013106 (1998)","journal-title":"Stud. Logica."},{"key":"16_CR28","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-540-32254-2_11","volume-title":"Mechanizing Mathematical Reasoning","author":"W Sieg","year":"2005","unstructured":"Sieg, W., Cittadini, S.: Normal natural deduction proofs (in non-classical logics). In: Hutter, D., Stephan, W. (eds.) Mechanizing Mathematical Reasoning. LNCS, vol. 2605, pp. 169\u2013191. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32254-2_11"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"S\u00f6rensen, M.H., Urzykzyn, P.: Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics. Elsevier (2006)","DOI":"10.1016\/S0049-237X(06)80005-4"},{"issue":"2","key":"16_CR30","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1006\/inco.1996.0027","volume":"125","author":"M Takahashi","year":"1996","unstructured":"Takahashi, M., Akama, Y., Hirokawa, S.: Normal proofs and their grammar. Inf. Comput. 125(2), 144\u2013153 (1996)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66997-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:05:34Z","timestamp":1748412334000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66997-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031669965","9783031669972"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66997-2_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"29 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"5 August 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 August 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2024\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}