{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T11:27:45Z","timestamp":1744111665310,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572616"},{"type":"electronic","value":"9783031572623"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>There has been much progress in designing bidirectional type systems and associated type synthesis algorithms, but mainly on a case-by-case basis. To remedy the situation, this paper develops a <jats:italic>general<\/jats:italic> and <jats:italic>formal<\/jats:italic> theory of bidirectional typing for simply typed languages: for every signature that specifies a mode-correct bidirectionally typed language, there exists a <jats:italic>proof-relevant<\/jats:italic> type synthesiser which, given an input abstract syntax tree, constructs a typing derivation if any, gives its refutation if not, or reports that the input does not have enough type annotations. Sufficient conditions for deriving a type synthesiser such as soundness, completeness, and mode-correctness are studied universally for all signatures. We propose a preprocessing step called <jats:italic>mode decoration<\/jats:italic>, which helps the user to deal with missing type annotations. The entire theory is formally implemented in <jats:sc>Agda<\/jats:sc>, so we provide a <jats:italic>verified<\/jats:italic> generator of proof-relevant type synthesisers as a by-product of our formalism.<\/jats:p>","DOI":"10.1007\/978-3-031-57262-3_5","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:02:35Z","timestamp":1712214155000},"page":"115-142","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Formal Treatment of Bidirectional Typing"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3250-1331","authenticated-orcid":false,"given":"Liang-Ting","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2439-1048","authenticated-orcid":false,"given":"Hsiang-Shang","family":"Ko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"5_CR1","unstructured":"Aczel, P.: A general Church\u2013Rosser theorem (1978),http:\/\/www.ens-lyon.fr\/LIP\/REWRITING\/MISC\/AGeneralChurch-RosserTheorem.pdf"},{"key":"5_CR2","unstructured":"Ahrens, B., Matthes, R., M\u00f6rtberg, A.: Implementing a category-theoretic"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Allais, G., Atkey, R., Chapman, J., McBride, C., McKinna, J.: A type- andscope-safe universe of syntaxes with binding: their semantics and proofs.Journal of Functional Programming 31, e22:1\u201355 (2021),https:\/\/doi.org\/10.1017\/S0956796820000076","DOI":"10.1017\/S0956796820000076"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Arkor, N., Fiore, M.: Algebraic models of simple type theories: a polynomialapproach. In: Symposium on Logic in Computer Science (LICS), pp. 88\u2013101, ACM(2020), https:\/\/doi.org\/10.1145\/3373718.3394771","DOI":"10.1145\/3373718.3394771"},{"key":"5_CR5","unstructured":"Assaf, A., Burel, G., Cauderlier, R., Delahaye, D., Dowek, G., Dubois, C.,"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Bauer, A., Haselwarter, P.G., Lumsdaine, P.L.: A general definition ofdependent type theories (2020), https:\/\/doi.org\/10.48550\/arXiv.2009.05539","DOI":"10.48550\/arXiv.2009.05539"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Bauer, A., Komel, A.P.: An extensible equality checking algorithm for dependenttype theories. Logical Methods in Computer Science 18(1), 17:1\u201342(2022), https:\/\/doi.org\/10.46298\/lmcs-18(1:17)2022","DOI":"10.46298\/lmcs-18(1:17)2022"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Chen, L.T., Ko, H.S.: A formal treatment of bidirectional typing (artefact)(2024), https:\/\/doi.org\/10.5281\/zenodo.10458840","DOI":"10.5281\/zenodo.10458840"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Dowek, G.: The undecidability of typability in the lambda-pi-calculus. In:International Conference on Typed Lambda Calculi and Applications (TLCA),Lecture Notes in Computer Science, vol. 664, pp. 139\u2013145, Springer (1993),https:\/\/doi.org\/10.1007\/BFb0037103","DOI":"10.1007\/BFb0037103"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Dunfield, J., Krishnaswami, N.: Bidirectional typing. ACM Computing Surveys54(5), 98:1\u201338 (2021), https:\/\/doi.org\/10.1145\/3450952","DOI":"10.1145\/3450952"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Felicissimo, T.: Generic bidirectional typing for dependent type theories(2023), https:\/\/doi.org\/10.48550\/arXiv.2307.08523","DOI":"10.48550\/arXiv.2307.08523"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Fiore, M., Hamana, M.: Multiversal polymorphic algebraic theories: syntax,semantics, translations, and equational logic. In: Symposium on Logic inComputer Science (LICS), pp. 520\u2013529, IEEE (2013),https:\/\/doi.org\/10.1109\/LICS.2013.59","DOI":"10.1109\/LICS.2013.59"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Fiore, M., Hur, C.K.: Second-order equational logic (extended abstract). In:International Workshop on Computer Science Logic (CSL), Lecture Notes inComputer Science, vol. 6247, pp. 320\u2013335, Springer (2010),https:\/\/doi.org\/10.1007\/978-3-642-15205-4_26","DOI":"10.1007\/978-3-642-15205-4_26"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Fiore, M., Szamozvancev, D.: Formal metatheory of second-order abstract syntax.Proceedings of the ACM on Programming Languages 6(POPL), 53:1\u201329(2022), https:\/\/doi.org\/10.1145\/3498715","DOI":"10.1145\/3498715"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Fiore, M.P., Plotkin, G.D., Turi, D.: Abstract syntax and variable binding. In:Symposium on Logic in Computer Science (LICS), pp. 193\u2013202, IEEE (1999),https:\/\/doi.org\/10.1109\/LICS.1999.782615","DOI":"10.1109\/LICS.1999.782615"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Hamana, M.: Polymorphic abstract syntax via Grothendieck construction. In:International Conference on Foundations of Software Science and ComputationalStructures (FoSSaCS), Lecture Notes in Computer Science, vol. 6604, pp.381\u2013395, Springer (2011), https:\/\/doi.org\/10.1007\/978-3-642-19805-2_26","DOI":"10.1007\/978-3-642-19805-2_26"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journalof the ACM 40(1), 143\u2013184 (1993), https:\/\/doi.org\/10.1145\/138027.138060","DOI":"10.1145\/138027.138060"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Harper, R., Licata, D.R.: Mechanizing metatheory in a logical framework.Journal of Functional Programming 17(4\u20135), 613\u2013673 (2007),https:\/\/doi.org\/10.1017\/S0956796807006430","DOI":"10.1017\/S0956796807006430"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Haselwarter, P.G., Bauer, A.: Finitary type theories with and without contexts(2021), https:\/\/doi.org\/10.48550\/arXiv.2112.00539","DOI":"10.48550\/arXiv.2112.00539"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Leivant, D.: Typing and computational properties of lambda expressions.Theoretical Computer Science 44, 51\u201368 (1986),https:\/\/doi.org\/10.1016\/0304-3975(86)90109-X","DOI":"10.1016\/0304-3975(86)90109-X"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"McBride, C.: First-order unification by structural recursion. Journal ofFunctional Programming 13(6), 1061\u20131075 (2003a),https:\/\/doi.org\/10.1017\/S0956796803004957","DOI":"10.1017\/S0956796803004957"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"McBride, C.: First-order unification by structural recursion: correctness proof(2003b),http:\/\/www.strictlypositive.org\/foubsr-website\/","DOI":"10.1017\/S0956796803004957"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Moggi, E.: Computational lambda-calculus and monads. In: Symposium on Logic inComputer Science (LICS), pp. 14\u201323, IEEE (1989),https:\/\/doi.org\/10.1109\/LICS.1989.39155","DOI":"10.1109\/LICS.1989.39155"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Pierce, B.C., Turner, D.N.: Local type inference. ACM Transactions onProgramming Languages and Systems 22(1), 1\u201344 (2000),https:\/\/doi.org\/10.1145\/345099.345100","DOI":"10.1145\/345099.345100"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Reed, J.: Redundancy elimination for LF. In: International Workshop onLogical Frameworks and Meta-Languages (LFM 2004), vol. 199, pp. 89\u2013106(2008), https:\/\/doi.org\/10.1016\/j.entcs.2007.11.014","DOI":"10.1016\/j.entcs.2007.11.014"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Tanaka, M., Power, A.J.: Pseudo-distributive laws and axiomatics for variablebinding. Higher-Order and Symbolic Computation 19(2\u20133), 305\u2013337(2006a), https:\/\/doi.org\/10.1007\/s10990-006-8750-x","DOI":"10.1007\/s10990-006-8750-x"},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Tanaka, M., Power, J.: A unified category-theoretic semantics for bindingsignatures in substructural logic. Journal of Logic and Computation16(1), 5\u201325 (2006b), https:\/\/doi.org\/10.1093\/logcom\/exi070","DOI":"10.1093\/logcom\/exi070"},{"key":"5_CR28","unstructured":"Uemura, T.: Abstract and Concrete Type Theories. Ph.D. thesis, University ofAmsterdam (2021),https:\/\/hdl.handle.net\/11245.1\/41ff0b60-64d4-4003-8182-c244a9afab3b"},{"key":"5_CR29","unstructured":"Univalent Foundations Program, T.: Homotopy Type Theory: UnivalentFoundations of Mathematics. Institute for Advanced Study (2013),https:\/\/homotopytypetheory.org\/book"},{"key":"5_CR30","unstructured":"Wadler, P., Kokke, W., Siek, J.G.: Programming Language Foundations inAgda (2022), https:\/\/plfa.inf.ed.ac.uk\/22.08\/"},{"key":"5_CR31","doi-asserted-by":"publisher","unstructured":"Wells, J.B.: Typability and type checking in System F are equivalent andundecidable. Annals of Pure and Applied Logic 98(1\u20133), 111\u2013156(1999), https:\/\/doi.org\/10.1016\/S0168-0072(98)00047-5","DOI":"10.1016\/S0168-0072(98)00047-5"},{"key":"5_CR32","doi-asserted-by":"publisher","unstructured":"Wood, J., Atkey, R.: A framework for substructural type systems. In: EuropeanSymposium on Programming (ESOP), Lecture Notes in Computer Science, vol.13240, pp. 376\u2013402, Springer (2022), https:\/\/doi.org\/10.1007\/978-3-030-99336-8_14","DOI":"10.1007\/978-3-030-99336-8_14"}],"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-3-031-57262-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:03:37Z","timestamp":1712214217000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57262-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572616","9783031572623"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57262-3_5","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":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","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":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"72","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":"25","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":"1","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":"35% - 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.2","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":"8","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)"}},{"value":"The proceedings also contain 4 artifact report that have not been part of the original submission","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}