{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T10:56:55Z","timestamp":1766401015399,"version":"3.41.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2018,10,31]],"date-time":"2018-10-31T00:00:00Z","timestamp":1540944000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["RA-18723-1 OAF"],"award-info":[{"award-number":["RA-18723-1 OAF"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2018,10,31]]},"abstract":"<jats:p>\n            M\n            <jats:sc>mt<\/jats:sc>\n            is a framework for designing and implementing formal systems in a way that systematically abstracts from theoretical and practical aspects of their type of theoretical and logical foundations. Thus, definitions, theorems, and algorithms can be stated independently of the foundation, and language designers can focus on the essentials of a particular foundation and inherit a large-scale implementation from M\n            <jats:sc>mt<\/jats:sc>\n            at low cost. Going beyond the similarly motivated approach of meta-logical frameworks, M\n            <jats:sc>mt<\/jats:sc>\n            does not even commit to a particular meta-logic\u2014that makes M\n            <jats:sc>mt<\/jats:sc>\n            level results harder to obtain but also more general.\n          <\/jats:p>\n          <jats:p>We present one such result: a type reconstruction algorithm that realizes the foundation-independent aspects generically relative to a set of rules that supply the foundation-specific knowledge. Maybe surprisingly, we see that the former covers most of the algorithm, including the most difficult details. Thus, we can easily instantiate our algorithm with rule sets for several important language features including, e.g., dependent function types. Moreover, our design is modular such that we obtain a type reconstruction algorithm for any combination of these features.<\/jats:p>","DOI":"10.1145\/3234693","type":"journal-article","created":{"date-parts":[[2018,12,10]],"date-time":"2018-12-10T13:09:16Z","timestamp":1544447356000},"page":"1-43","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["A Modular Type Reconstruction Algorithm"],"prefix":"10.1145","volume":"19","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3040-3655","authenticated-orcid":false,"given":"Florian","family":"Rabe","sequence":"first","affiliation":[{"name":"University Erlangen-Nuremberg, Erlangen, Germany"}]}],"member":"320","published-online":{"date-parts":[[2018,12,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"A. Asperti C. Sacerdoti Coen E. Tassi and S. Zacchiroli. 2006. Crafting a proof assistant. In TYPES T. Altenkirch and C. McBride (Eds.). Springer 18--32.   A. Asperti C. Sacerdoti Coen E. Tassi and S. Zacchiroli. 2006. Crafting a proof assistant. In TYPES T. Altenkirch and C. McBride (Eds.). Springer 18--32.","DOI":"10.1007\/978-3-540-74464-1_2"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00245294"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_8"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:18)2012"},{"volume-title":"Proceedings of PxTP2012: Proof Exchange for Theorem Proving, D. Pichardie and T. Weber (Eds.). 28--43","author":"Boespflug M.","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_7_1","first-page":"101","article-title":"Hammering towards QED","volume":"9","author":"Blanchette J.","year":"2016","journal-title":"Journal of Formalized Reasoning"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951932"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"D. Cousineau and G. Dowek. 2007. Embedding pure type systems in the lambda-pi-calculus modulo. In Typed Lambda Calculi and Applications S. Ronchi Della Rocca (Ed.). Springer. 102--117.   D. Cousineau and G. Dowek. 2007. Embedding pure type systems in the lambda-pi-calculus modulo. In Typed Lambda Calculi and Applications S. Ronchi Della Rocca (Ed.). Springer. 102--117.","DOI":"10.1007\/978-3-540-73228-0_9"},{"key":"e_1_2_1_11_1","unstructured":"Coq Development Team. 2015. The Coq Proof Assistant: Reference Manual. Technical report INRIA.  Coq Development Team. 2015. The Coq Proof Assistant: Reference Manual. Technical report INRIA."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_32"},{"key":"e_1_2_1_13_1","unstructured":"L. de Moura J. Avigad S. Kong and C. Roux. 2015. Elaboration in dependent type theory. Retrieved from https:\/\/arxiv.org\/abs\/1505.04324.  L. de Moura J. Avigad S. Kong and C. Roux. 2015. Elaboration in dependent type theory. Retrieved from https:\/\/arxiv.org\/abs\/1505.04324."},{"volume-title":"The lean theorem prover (system description)","author":"de Moura L.","key":"e_1_2_1_14_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110278"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2643135.2643153"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022971915900"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_13"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_23"},{"volume-title":"Technical Report RR-6455, INRIA.","year":"2008","author":"Gonthier G.","key":"e_1_2_1_20_1"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"volume-title":"Work-in-Progress Proceedings, A. Asperti, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.)","author":"Horozal F.","key":"e_1_2_1_22_1"},{"key":"e_1_2_1_23_1","first-page":"3","article-title":"LLFP: A logical framework for modeling external evidence, side conditions, and proof irrelevance using monads","volume":"13","author":"Honsell F.","year":"2017","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)90009-4"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31374-5_22"},{"key":"e_1_2_1_26_1","unstructured":"M. Kohlhase T. Mossakowski and F. Rabe. 2009. The LATIN Project. Retrieved from https:\/\/trac.omdoc.org\/LATIN\/.  M. Kohlhase T. Mossakowski and F. Rabe. 2009. The LATIN Project. Retrieved from https:\/\/trac.omdoc.org\/LATIN\/."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11856290_21"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-014-0182-0"},{"volume-title":"More on implicit syntax","author":"Luther M.","key":"e_1_2_1_29_1","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45744-5_31"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9085-y"},{"key":"e_1_2_1_31_1","unstructured":"U. Norell. 2005. The Agda WiKi. Retrieved from http:\/\/wiki.portal.chalmers.se\/agda.  U. Norell. 2005. The Agda WiKi. Retrieved from http:\/\/wiki.portal.chalmers.se\/agda."},{"volume-title":"11th International Conference on Automated Deduction (CADE\u201992)","author":"Owre S.","key":"e_1_2_1_32_1"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000408"},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"F. Pfenning and C. Sch\u00fcrmann. 1999. System description: Twelf - a meta-logical framework for deductive systems. In Automated Deduction H. Ganzinger (Ed.). 202--206.   F. Pfenning and C. Sch\u00fcrmann. 1999. System description: Twelf - a meta-logical framework for deductive systems. In Automated Deduction H. Ganzinger (Ed.). 202--206.","DOI":"10.1007\/3-540-48660-7_14"},{"volume-title":"International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, A. Abel and C. Urban (Eds.). ENTCS, 135--141","author":"Poswolsky A.","key":"e_1_2_1_37_1"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31374-5_10"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39320-4_25"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.167.7"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-20615-8_7"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu079"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2013.06.001"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1577824.1577831"},{"volume-title":"Theorem Proving in Higher Order Logics","author":"Wenzel M.","key":"e_1_2_1_45_1"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3234693","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3234693","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:57:48Z","timestamp":1750208268000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3234693"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,31]]},"references-count":44,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,10,31]]}},"alternative-id":["10.1145\/3234693"],"URL":"https:\/\/doi.org\/10.1145\/3234693","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2018,10,31]]},"assertion":[{"value":"2017-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-12-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}