SpringerLink
Log in

Logical Frameworks—A Brief Introduction

  • Chapter
Proof and System-Reliability

Part of the book series: NATO Science Series ((NAII,volume 62))

Abstract

A logical framework is a meta-language for the formalization of deductive systems. We provide a brief introduction to logical frameworks and their methodology, concentrating on LF. We use first-order logic as the running example to illustrate the representations of syntax, natural deductions, and proof transformations.

We also sketch a recent formulation of LF centered on the notion of canonical form, and show how it affects proofs of adequacy of encodings.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

eBook
EUR 9.99
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 53.49
Price includes VAT (Germany)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  • Altenkirch, T., V. Gaspes, B. Nordström, and B. von Sydow: 1994, ‘A User’s Guide to ALF’. Chalmers University of Technology, Sweden.

    Google Scholar 

  • Barendregt, H. P.: 1980, The Lambda-Calculus: Its Syntax and Semantics. North-Holland.

    Google Scholar 

  • Basin, D. and S. Matthews: 1996, ‘Structuring Metatheory on Inductive Definitions’. In:M. McRobbie and J. Slaney (eds.): Proceedings of the 13th International Conference on Automated Deduction (CADE-13). New Brunswick, New Jersey, pp. 171–185, Springer-Verlag LNAI 1104.

    Google Scholar 

  • Basin, D. and S. Matthews: 2001, ‘Logical Frameworks’. In: D. Gabbay and F. Guenthner (eds.): Handbook of Philosophical Logic. Kluwer Academic Publishers, 2nd edition. In preparation.

    Google Scholar 

  • Basin, D. A. and R. L. Constable: 1993, ‘Metalogical Frameworks’. In: G. Huet and G.Plotkin (eds.): Logical Environments. Cambridge University Press, pp. 1–29.

    Google Scholar 

  • Cervesato, I. and F. Pfenning: 1996, ‘A Linear Logical Framework’. In: E. Clarke (ed.):Proceedings of the Eleventh Annual Symposium on Logic in Computer Science. New Brunswick, New Jersey, pp. 264–275, IEEE Computer Society Press.

    Chapter  Google Scholar 

  • Cervesato, I. and F. Pfenning: 1997, ‘Linear Higher-Order Pre-Unification’. In: G.Winskel (ed.): Proceedings of the Twelfth Annual Sumposium on Logic in Computer Science (LICS’97). Warsaw, Poland, pp. 422–433, IEEE Computer Society Press.

    Chapter  Google Scholar 

  • de Bruijn, N.: 1968, ‘The Mathematical Language AUTOMATH, Its Usage, and Some of Its Extensions’. In: M. Laudet (ed.): Proceedings of the Symposium on Automatic Demonstration. Versailles, France, pp. 29–61, Springer-Verlag LNM 125.

    Google Scholar 

  • de Bruijn, N.: 1991, ‘A Plea for Weaker Frameworks’. In: G. Huet and G. Plotkin (eds.):Logical Frameworks, pp. 40–67, Cambridge University Press.

    Chapter  Google Scholar 

  • de Bruijn, N.: 1993, ‘Algorithmic Definition of Lambda-Typed Lambda Calculus’. In:G. Huet and G. Plotkin (eds.): Logical Environment. Cambridge University Press, pp.131–145.

    Google Scholar 

  • Dowek, G.: 1993, ‘The Undecidability of Typability in the Lambda-Pi-Calculus’. In:M. Bezem and J. Groote (eds.): Proceedings of the International Conference on Typed Lambda Calculi and Applications. Utrecht, The Netherlands, pp. 139–145, Springer-Verlag LNCS 664.

    Chapter  Google Scholar 

  • Eriksson, L.-H.: 1994, ‘Pi: An Interactive Derivation Editor for the Calculus of Partial Inductive Definitions’. In: A. Bundy (ed.): Proceedings of the 12th International Conference on Automated Deduction. Nancy, Prance, pp. 821–825, Springer Verlag LNAI 814.

    Google Scholar 

  • Feferman, S.: 1988, ‘Finitary Inductive Systems’. In: R. Ferro (ed.): Proceedings of Logic Colloquium ’88. Padova, Italy, pp. 191–220, North-Holland.

    Google Scholar 

  • Felty, A.: 1991, ‘Encoding Dependent Types in an Intuitionistic Logic’. In: G. Huet and G. D. Plotkin (eds.): Logical Frameworks, pp. 214–251, Cambridge University Press.

    Google Scholar 

  • Felty, A. and D. Miller: 1988, ‘Specifying Theorem Provers in a Higher-Order Logic Programming Language’.In: E. Lusk and R. Overbeek (eds.): Proceedings of the Ninth International Conference on Automated Deduction. Argonne, Illinois, pp. 61–80, Springer-Verlag LNCS 310.

    Chapter  Google Scholar 

  • Gabbay, D. M.: 1994, ‘Classical vs Non-Classical Logic’. In: D. Gabbay, C. Hogger, and J. Robinson (eds.): Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 2. Oxford University Press, Chapt. 2.6.

    Google Scholar 

  • Harper, R., F. Honsell, and G. Plotkin: 1993, ‘A Framework for Defining Logics’. Journal of the Association for Computing Machinery 40(1), 143–184.

    Article  MathSciNet  MATH  Google Scholar 

  • Howard, W. A.: 1980, ‘The formulae-as-types notion of construction’. In: J. P. Seldin and J. R. Hindley (eds.): To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, pp. 479–490. Hitherto unpublished note of 1969.

    Google Scholar 

  • Martì-Oliet, N. and J. Meseguer: 1993, ‘Rewriting Logic as a Logical and Semantical Framework’. Technical Report SRI-CSL-93-05, SRI International.

    Google Scholar 

  • Martin-Löf, P.: 1980, ‘Constructive Mathematics and Computer Programming’. In: Logic, Methodology and Philosophy of Science VI. pp. 153-175, North–Holland.

    Google Scholar 

  • Martin-Löf, P.: 1985, ‘On the Meanings of the Logical Constants and the Justifications of the Logical Laws’. Technical Report 2, Scuola di Specializzazione in Logica Matematica, Dipartimento di Matematica, Università di Siena. Reprinted in the Nordic Journal of Philosophical Logic, 1(1), 11–60, 1996.

    Google Scholar 

  • McDowell, R. and D. Miller: 1997, ‘A Logic for Reasoning with Higher-Order Abstract Syntax’. In: G. Winskel (ed.): Proceedings of the Twelfth Annual Symposium on Logic in Computer Science. Warsaw, Poland, pp. 434–445, IEEE Computer Society Press.

    Chapter  Google Scholar 

  • Miller, D.: 1994, ‘A Multiple-Conclusion Meta-Logic’.In: S. Abramsky (ed.): Ninth Annual Symposium on Logic in Computer Science. Paris, France, pp. 272–281, IEEE Computer Society Press.

    Chapter  Google Scholar 

  • Nadathur, G. and D. Miller: 1988, ‘An Overview of λProlog’. In: K. A. Bowen and R. A. Kowalski (eds.): Fifth International Logic Programming Conference. Seattle, Washington, pp. 810–827, MIT Press.

    Google Scholar 

  • Necula, G. C: 1997, ‘Proof-Carrying Code’. In: N. D. Jones (ed.): Conference Record of the 24th Symposium on Principles of Programming Languages (POPL’97). Paris, France, pp. 106–119, ACM Press.

    Google Scholar 

  • Necula, G. C: 2002, ‘Proof-Carrying Code: Design and Implementation’. This volume. Kluwer Academic Publishers.

    Google Scholar 

  • Nordström, B., K. Petersson, and J. M. Smith: 1990, Programming in Martin-Löf ’s Type Theory: An Introduction. Oxford University Press.

    MATH  Google Scholar 

  • Paulson, L. C: 1986, ‘Natural Deduction as Higher-order Resolution’. Journal of Logic Programming 3, 237–258.

    Article  MathSciNet  MATH  Google Scholar 

  • Pfenning, F.: 1991, ‘Logic Programming in the LF Logical Framework’. In: G. Huet and G. Plotkin (eds.): Logical Frameworks. pp. 149–181, Cambridge University Press.

    Chapter  Google Scholar 

  • Pfenning, F.: 1996, ‘The Practice of Logical Frameworks’. In: H. Kirchner (ed.): Proceedings of the Colloquium on Trees in Algebra and Programming. Linkö**, Sweden, pp. 119–134, Springer-Verlag LNCS 1059. Invited talk.

    Chapter  Google Scholar 

  • Pfenning, F.: 2000, ‘Structural Cut Elimination I. Intuitionistic and Classical Logic’. Information and Computation 157(1/2), 84–141.

    Article  MathSciNet  MATH  Google Scholar 

  • Pfenning, F.: 2001a,Computation and Deduction.Cambridge University Press.In preparation. Draft from April 1997 available electronically.

    Google Scholar 

  • Pfenning, F.: 2001b, ‘Logical Frameworks’. In: A. Robinson and A. Voronkov (eds.): Handbook of Automated Reasoning.Elsevier Science and MIT Press, Chapt. 16, pp. 977–1061. In press.

    Google Scholar 

  • Pfenning, F. and C. Schürmann: 1999, ‘System Description: Twelf - A Meta-Logical Framework for Deductive Systems’. In: H. Ganzinger (ed.): Proceedings of the 16th International Conference on Automated Deduction (CADE-16). Trento, Italy, pp. 202–206,Springer-Verlag LNAI 1632.

    Google Scholar 

  • Schürmann, C.: 2000, ‘Automating the Meta Theory of Deductive Systems’. Ph.D. thesis, Department of Computer Science, Carnegie Mellon University. Available as Technical Report CMU-CS-00-146.

    Google Scholar 

  • Watkins, K., I. Cervesato, F. Pfenning, and D. Walker: 2002, ‘A Concurrent Logical Framework I: Judgments and Properties’.Technical Report CMU-CS-02-101, Department of Computer Science, Carnegie Mellon University. Forthcoming.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Carnegie Mellon University, USA

    Frank Pfenning

Authors
  1. Frank Pfenning
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Mathematisches Institut, Ludwig-Maximilians-Universität, München, Germany

    Helmut Schwichtenberg

  2. Institut für Informatik, Technische Universität, München, Germany

    Ralf Steinbrüggen

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer Science+Business Media Dordrecht

About this chapter

Cite this chapter

Pfenning, F. (2002). Logical Frameworks—A Brief Introduction. In: Schwichtenberg, H., Steinbrüggen, R. (eds) Proof and System-Reliability. NATO Science Series, vol 62. Springer, Dordrecht. https://doi.org/10.1007/978-94-010-0413-8_5

Download citation

  • DOI: https://doi.org/10.1007/978-94-010-0413-8_5

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-1-4020-0608-1

  • Online ISBN: 978-94-010-0413-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation