{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:23Z","timestamp":1774837823441,"version":"3.50.1"},"reference-count":60,"publisher":"Cambridge University Press (CUP)","issue":"4-5","license":[{"start":{"date-parts":[[2007,7,1]],"date-time":"2007-07-01T00:00:00Z","timestamp":1183248000000},"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":[[2007,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The LF logical framework codifies a methodology for representing deductive systems, such as programming languages and logics, within a dependently typed \u03bb-calculus. In this methodology, the syntactic and deductive apparatus of a system is encoded as the canonical forms of associated LF types; an encoding is correct (<jats:italic>adequate<\/jats:italic>) if and only if it defines a<jats:italic>compositional bijection<\/jats:italic>between the apparatus of the deductive system and the associated canonical forms. Given an adequate encoding, one may establish metatheoretic properties of a deductive system by reasoning about the associated LF representation. The Twelf implementation of the LF logical framework is a convenient and powerful tool for putting this methodology into practice. Twelf supports both the representation of a deductive system and the mechanical verification of proofs of metatheorems about it. The purpose of this article is to provide an up-to-date overview of the LF \u03bb-calculus, the LF methodology for adequate representation, and the Twelf methodology for mechanizing metatheory. We begin by defining a variant of the original LF language, called<jats:italic>Canonical LF<\/jats:italic>, in which only canonical forms (long \u03b2\u03b7-normal forms) are permitted. This variant is parameterized by a<jats:italic>subordination relation<\/jats:italic>, which enables modular reasoning about LF representations. We then give an adequate representation of a simply typed \u03bb-calculus in Canonical LF, both to illustrate adequacy and to serve as an object of analysis. Using this representation, we formalize and verify the proofs of some metatheoretic results, including preservation, determinacy, and strengthening. Each example illustrates a significant aspect of using LF and Twelf for formalized metatheory.<\/jats:p>","DOI":"10.1017\/s0956796807006430","type":"journal-article","created":{"date-parts":[[2007,7,6]],"date-time":"2007-07-06T08:38:02Z","timestamp":1183711082000},"page":"613-673","source":"Crossref","is-referenced-by-count":61,"title":["Mechanizing metatheory in a logical framework"],"prefix":"10.1017","volume":"17","author":[{"given":"ROBERT","family":"HARPER","sequence":"first","affiliation":[]},{"given":"DANIEL R.","family":"LICATA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2007,7,1]]},"reference":[{"key":"S0956796807006430_ref60","unstructured":"Watkins K. , Cervesato I. , Pfenning F. & Walker D. (2004b) Specifying properties of concurrent computations in CLF. In International Workshop on Logical Frameworks and Meta-Languages, Sch\u00fcrmann C. (ed)."},{"key":"S0956796807006430_ref57","unstructured":"Virga R. (1999) Higher-Order Rewriting with Dependent Types, Ph.D. thesis. Pittsburgh, PA: Carnegie Mellon University."},{"key":"S0956796807006430_ref54","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_25"},{"key":"S0956796807006430_ref51","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_8"},{"key":"S0956796807006430_ref50","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1007\/BFb0054266","volume-title":"International Conference on Automated Deduction.","author":"Sch\u00fcrmann","year":"1998"},{"key":"S0956796807006430_ref49","unstructured":"Sch\u00fcrmann C. (2000) Automating the Meta-theory of Deductive Systems, Ph.D. thesis. Pittsburgh, PA: Carnegie Mellon University."},{"key":"S0956796807006430_ref47","first-page":"296","volume-title":"European Symposium on Programming","author":"Rohwedder","year":"1996"},{"key":"S0956796807006430_ref46","first-page":"135","volume-title":"International Workshop on Hybrid Logic.","author":"Reed","year":"2006"},{"key":"S0956796807006430_ref56","unstructured":"van Daalen D. T. (1980) The Language Theory of AUTOMATH, Ph.D. thesis. Eindhoven, Netherlands: Technical University of Eindhoven."},{"key":"S0956796807006430_ref45","unstructured":"Pientka B. & Pfenning F. (2000) Termination and reduction checking in the logical framework. In Workshop on Automation of Proofs by Mathematical Induction. Sch\u00fcrmann C. (ed)."},{"key":"S0956796807006430_ref44","unstructured":"Pfenning F. & Sch\u00fcrmann C. (2002) Twelf User's Guide, Version 1.4."},{"key":"S0956796807006430_ref42","first-page":"537","volume-title":"International Conference on Automated Deduction.","author":"Pfenning","year":"1992"},{"key":"S0956796807006430_ref41","volume-title":"Handbook of Automated Reasoning","author":"Pfenning","year":"1999"},{"key":"S0956796807006430_ref40","volume-title":"A Structural Proof of Cut Elimination and Its Representation in A Logical Framework.","author":"Pfenning","year":"1994"},{"key":"S0956796807006430_ref39","doi-asserted-by":"publisher","DOI":"10.21236\/ADA256574"},{"key":"S0956796807006430_ref31","unstructured":"Miculan M. (1997) Encoding Logical Theories of Programs, Ph.D. thesis. Pisa, Italy: Dipartimento di Informatica, Universita di Pisa."},{"key":"S0956796807006430_ref27","first-page":"173","volume-title":"ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.","author":"Lee","year":"2007"},{"key":"S0956796807006430_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"S0956796807006430_ref25","volume-title":"Computer-Aided Reasoning: An Approach","author":"Kaufmann","year":"2000"},{"key":"S0956796807006430_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"S0956796807006430_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/1042038.1042041"},{"key":"S0956796807006430_ref35","doi-asserted-by":"crossref","unstructured":"Nanevski A. , Pfenning F. & Pientka B. (to appear) Contextual modal type theory. ACM Transactions on Computational Logic.","DOI":"10.1145\/1352582.1352591"},{"key":"S0956796807006430_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_14"},{"key":"S0956796807006430_ref20","first-page":"453","volume-title":"IEEE Symposium on Logic in Computer Science.","author":"Geuvers","year":"1992"},{"key":"S0956796807006430_ref19","doi-asserted-by":"crossref","unstructured":"Garg D. & Pfenning F. (2006) Non-interference in constructive authorization logic. In Computer Security Foundations Workshop, pp. 183\u2013293.","DOI":"10.1109\/CSFW.2006.18"},{"key":"S0956796807006430_ref17","first-page":"214","volume-title":"Logical Frameworks","author":"Felty","year":"1991"},{"key":"S0956796807006430_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569807.011"},{"key":"S0956796807006430_ref1","volume-title":"European Symposium on Programming","author":"Acar","year":"2007"},{"key":"S0956796807006430_ref14","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1145\/604131.604149","volume-title":"ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Crary","year":"2003"},{"key":"S0956796807006430_ref15","first-page":"106","volume-title":"International Conference on Automated Deduction.","author":"Crary","year":"2003"},{"key":"S0956796807006430_ref55","unstructured":"Simmons R. (2005) Twelf as a Unified Framework for Language Formalization and Implementation. Tech. rept. Princetn, NJ: Princeton University. Undergraduate Senior Thesis 18679."},{"key":"S0956796807006430_ref18","first-page":"7","volume-title":"European Symposium on Programming.","author":"Fluet","year":"2006"},{"key":"S0956796807006430_ref43","doi-asserted-by":"crossref","unstructured":"Pfenning F. & Sch\u00fcrmann C. (1999) System description: Twelf \u2014 a meta-logical framework for deductive systems. In International Conference on Automated Deduction, Ganzinger H. (ed). pp. 202\u2013206.","DOI":"10.1007\/3-540-48660-7_14"},{"key":"S0956796807006430_ref58","doi-asserted-by":"crossref","unstructured":"Watkins K. Cervesato I. , Pfenning F. & Walker D. (2002 A Concurrent Logical Framework I: Judgments and Properties. Tech. rept. CMU-CS-02-101. Pittsburgh PA: Department of Computer Science, Carnegie Mellon University. Revised May 2003.","DOI":"10.21236\/ADA418517"},{"key":"S0956796807006430_ref34","unstructured":"Nanevski A. & Morrisett G. (2006) Dependent type theory of stateful higher-order functions. Tech. rept. TR-24-05. Cambridge, MA: Harvard Computer Science."},{"key":"S0956796807006430_ref32","first-page":"286","volume-title":"IEEE Symposium on Logic in Computer Science.","author":"Murphy","year":"2004"},{"key":"S0956796807006430_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0031814"},{"key":"S0956796807006430_ref53","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00280-4"},{"key":"S0956796807006430_ref9","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2951"},{"key":"S0956796807006430_ref3","first-page":"247","volume-title":"IEEE Symposium on Logic in Computer Science","author":"Appel","year":"2001"},{"key":"S0956796807006430_ref37","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic.","author":"Nipkow","year":"2002"},{"key":"S0956796807006430_ref48","unstructured":"Salvesen A. (1990) The Church-Rosser theorem for LF with \u03b2\u03b7-reduction. Unpublished notes to a talk given at the First Workshop on Logical Frameworks."},{"key":"S0956796807006430_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30142-4_2"},{"key":"S0956796807006430_ref30","first-page":"299","volume-title":"International Workshop on Extensions of Logic Programming","author":"Michaylov","year":"1991"},{"key":"S0956796807006430_ref10","unstructured":"Cervesato I. , Pfenning F. , Walker D. & Watkins K. (2002) A Concurrent Logical Framework II: Examples and Applications. Tech. rept. CMU-CS-02-102. Pittsburgh PA: Department of Computer Science, Carnegie Mellon University. Revised May 2003."},{"key":"S0956796807006430_ref5","unstructured":"Appel A. & Leroy X. (2006) A list-machine benchmark for mechanized metatheory. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice. Electronic Notes in Theoretical Computer Science, 95\u2013108."},{"key":"S0956796807006430_ref28","first-page":"42","volume-title":"ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.","author":"Leroy","year":"2006"},{"key":"S0956796807006430_ref29","volume-title":"A Formulation of Dependent ML With Explicit Equality Proofs.","author":"Licata","year":"2005"},{"key":"S0956796807006430_ref16","first-page":"131","volume-title":"Logical Environment.","author":"de Bruijn","year":"1993"},{"key":"S0956796807006430_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/11538363_6"},{"key":"S0956796807006430_ref52","first-page":"150","volume-title":"International Conference on Logic for Programming Artificial Intelligence and Reasoning.","author":"Sch\u00fcrmann","year":"2005"},{"key":"S0956796807006430_ref38","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569807.008"},{"key":"S0956796807006430_ref59","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_23"},{"key":"S0956796807006430_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004921"},{"key":"S0956796807006430_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3658-0_8"},{"key":"S0956796807006430_ref36","volume-title":"Selected papers on AUTOMATH","author":"Nederpelt","year":"1994"},{"key":"S0956796807006430_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"S0956796807006430_ref8","volume-title":"Texts in Theoretical Computer Science.","author":"Bertot","year":"2004"},{"key":"S0956796807006430_ref11","volume-title":"Implementing Mathematics With the NuPRL Proof Development System","author":"Constable","year":"1986"},{"key":"S0956796807006430_ref12","unstructured":"Coq Development Team. (2007) The Coq Proof Assistant Reference Manual. INRIA. Available at: http:\/\/coq.inria.fr. Accessed June, 2007."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796807006430","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T00:49:53Z","timestamp":1556585393000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796807006430\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,7]]},"references-count":60,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2007,7]]}},"alternative-id":["S0956796807006430"],"URL":"https:\/\/doi.org\/10.1017\/s0956796807006430","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,7]]}}}