{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:47Z","timestamp":1779836747995,"version":"3.53.1"},"reference-count":39,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2012,11,2]],"date-time":"2012-11-02T00:00:00Z","timestamp":1351814400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2013,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Although type reconstruction for dependently typed languages is common in practical systems, it is still ill-understood. Detailed descriptions of the issues around it are hard to find and formal descriptions together with correctness proofs are non-existing. In this paper, we discuss a one-pass type reconstruction for objects in the logical framework LF, describe formally the type reconstruction process using the framework of contextual modal types, and prove correctness of type reconstruction. Since type reconstruction will find most general types and may leave free variables, we in addition describe abstraction which will return a closed object where all free variables are bound at the outside. We also implemented our algorithms as part of the Beluga language, and the performance of our type reconstruction algorithm is comparable to type reconstruction in existing systems such as the logical framework Twelf.<\/jats:p>","DOI":"10.1017\/s0956796812000408","type":"journal-article","created":{"date-parts":[[2012,11,6]],"date-time":"2012-11-06T06:09:43Z","timestamp":1352182183000},"page":"1-37","source":"Crossref","is-referenced-by-count":9,"title":["An insider's look at LF type reconstruction: everything you (n)ever wanted to know"],"prefix":"10.1017","volume":"23","author":[{"given":"BRIGITTE","family":"PIENTKA","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2012,11,2]]},"reference":[{"key":"S0956796812000408_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_8"},{"key":"S0956796812000408_ref34","first-page":"135","volume-title":"Proceedings of the International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP'08)","author":"Poswolsky","year":"2009"},{"key":"S0956796812000408_ref32","unstructured":"Pollack R. (1990). Implicit syntax. Proceedings of First Workshop on Logical Frameworks, Eds. G. Huet and G. Plotkin , pp 421\u2013435"},{"key":"S0956796812000408_ref30","first-page":"163","volume-title":"Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'08)","author":"Pientka","year":"2008"},{"key":"S0956796812000408_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328483"},{"key":"S0956796812000408_ref27","unstructured":"Pientka B. (2003) Tabled Higher-Order Logic Programming. PhD. thesis, Department of Computer Science, Carnegie Mellon University. CMU-CS-03-185."},{"key":"S0956796812000408_ref39","volume-title":"A Concurrent Logical Framework I: Judgments and Properties","author":"Watkins","year":"2002"},{"key":"S0956796812000408_ref25","volume-title":"Computation and Deduction","author":"Pfenning","year":"2012"},{"key":"S0956796812000408_ref24","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569807.008"},{"key":"S0956796812000408_ref23","unstructured":"Norell U. (2007 September) Towards a Practical Programming Language Based on Dependent Type Theory. PhD. thesis, Department of Computer Science and Engineering, Chalmers University of Technology. Technical Report 33D."},{"key":"S0956796812000408_ref22","first-page":"93","volume-title":"Proceedings of the 13th Annual Symposium on Logic in Computer Science (LICS'98)","author":"Necula","year":"1998"},{"key":"S0956796812000408_ref21","first-page":"106","volume-title":"Proceedings of the 24th Annual Symposium on Principles of Programming Languages (POPL'97)","author":"Necula","year":"1997"},{"key":"S0956796812000408_ref16","first-page":"386","volume-title":"Proceedings of the First International Joint Conference on Automated Reasoning (IJCAR'01)","author":"Luther","year":"2001"},{"key":"S0956796812000408_ref15","first-page":"241","volume-title":"Proceedings of the 23rd Symposium on Logic in Computer Science","author":"Licata","year":"2008"},{"key":"S0956796812000408_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006430"},{"key":"S0956796812000408_ref33","first-page":"93","volume-title":"Proceedings of the 17th European Symposium on Programming (ESOP '08)","author":"Poswolsky","year":"2008"},{"key":"S0956796812000408_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037103"},{"key":"S0956796812000408_ref17","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"S0956796812000408_ref18","first-page":"255","volume-title":"Proceedings of the 8th International Logic Programming Conference","author":"Miller","year":"1991"},{"key":"S0956796812000408_ref36","doi-asserted-by":"publisher","DOI":"10.1145\/1577824.1577832"},{"key":"S0956796812000408_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0032392"},{"key":"S0956796812000408_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190245"},{"key":"S0956796812000408_ref31","first-page":"15","volume-title":"Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR'10)","author":"Pientka","year":"2010"},{"key":"S0956796812000408_ref35","first-page":"89","volume-title":"4th Workshop on Logical Frameworks and Meta-Languages (LFM'04)","author":"Reed","year":"2004"},{"key":"S0956796812000408_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"S0956796812000408_ref6","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/13.5.639"},{"key":"S0956796812000408_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_19"},{"key":"S0956796812000408_ref9","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1995.523271"},{"key":"S0956796812000408_ref3","first-page":"365","volume-title":"Proceedings of the 11th International Conference on Foundations of Software Science and Computational Structures (FOSSACS'08)","author":"Barras","year":"2008"},{"key":"S0956796812000408_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_27"},{"key":"S0956796812000408_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"S0956796812000408_ref26","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"16th International Conference on Automated Deduction (CADE-16)","author":"Pfenning","year":"1999"},{"key":"S0956796812000408_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"S0956796812000408_ref38","unstructured":"Virga R. (1999) Higher-Order Rewriting with Dependent Types. PhD. thesis, Department of Mathematical Sciences, Carnegie Mellon University. CMU-CS-99-167."},{"key":"S0956796812000408_ref10","first-page":"259","volume-title":"Proceedings of the Joint International Conference and Symposium on Logic Programming","author":"Dowek","year":"1996"},{"key":"S0956796812000408_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604149"},{"key":"S0956796812000408_ref1","first-page":"31","volume-title":"Proceedings of the 17th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Abadi","year":"1990"},{"key":"S0956796812000408_ref2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/1328438.1328443","volume-title":"Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Aydemir","year":"2008"},{"key":"S0956796812000408_ref5","unstructured":"Boespflug M. (2010) Dedukti. Available at: http:\/\/www.lix.polytechnique.fr\/dedukti"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796812000408","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:28Z","timestamp":1779834988000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796812000408\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,11,2]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,1]]}},"alternative-id":["S0956796812000408"],"URL":"https:\/\/doi.org\/10.1017\/s0956796812000408","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,11,2]]}}}