A framework for defining logics

ABSTRACT

The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed &lgr;-calculus with dependent types. Syntax is treated in a style similar to, but more general than, Martin-Lo¨f's system of arities. The treatment of rules and proofs focuses on his notion of a judgment. Logics are represented in LF via a new principle, the judgments as types principle, whereby each judgment is identified with the type of its proofs. This allows for a smooth treatment of discharge and variable occurence conditions and leads to a uniform treatment of rules and proofs whereby rules are viewed as proofs of higher-order judgments and proof checking is reduced to type checking. The practical benefit of our treatment of formal systems is that logic-independent tools, such as proof editors and proof checkers, can be constructed.

REFERENCES

• 1: ~ANDREWS, P.B. Resolution in type theory. J. Symb. Logic 36 (1971), 414-432.
• 2: Arnon Avron, Simple consequence relations, Information and Computation, v.92 n.1, p.105-139, May 1991 [doi>10.1016/0890-5401(91)90023-U]
• 3: Arnon Avron , Furio Honsell , Ian A. Mason, An overview of the Edinburgh logical framework, Current trends in hardware verification and automated theorem proving, Springer-Verlag New York, Inc., New York, NY, 1989
• 4: Arnon Avron , Furio Honsell , Ian A. Mason , Robert Pollack, Using typed lambda calculus to implement formal systems on a machine, Journal of Automated Reasoning, v.9 n.3, p.309-354, Dec. 1992 [doi>10.1007/BF00245294]
• 5: Rod Burstall , Furio Honsell, Operational semantics in a natural deduction setting, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 6: ~CHURCH, A. A formulation of the simple theory of types. J. Svmb Logzc 5 (1940), 56-68.
• 7: ~CLOCKSIN, W., AND MELLiSH, C.S. Progratnmbtg ill PROLOG. Spnnger-Verlag, New York, ~1981.
• 8: ~CONSTABLE, R., AND HOWE, D. NuPRL as a general logic. In Logic and Colnputahon, P. ~Odifreddi, Ed. Academic Press, Orlando, Fla., pp. 77 90.
• 9: R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , S. F. Smith, Implementing mathematics with the Nuprl proof development system, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
• 10: ~COQUAND, T. Une Th'eorie des Constructions. Ph.D dissertation. UniversitY' Paris VII, Paris, ~France, Jan. 1985.
• 11: Thierry Coquand, An algorithm for testing conversion in type theory, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 12: Thierry Coquand , Gérard P. Huet, Constructions: A Higher Order Proof System for Mechanizing Mathematics, Invited Lectures from the European Conference on Computer Algebra-Volume I, p.151-184, April 01-03, 1985
• 13: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• 14: ~CURRY, H. B., AND FEYS, R. Cognbinatory Logic. North-Holland, Amsterdam, The Nether- ~lands, 1958.
• 15: ~DE BRUIJN, N. G. A survey of the project AUTOMATH. In To H. B. Curry: Essays in ~Combinatory Logic, Lambda Calculus and Fotmalisnz, J. P. Seddin and J. R. Hindley, Eds. ~Academic Press, New York, 1980, pp. 589-606.
• 16: ~ELUOTT, C. Extensions and applications of higher-order unification, PhD dissertation. ~School of Computer Science, Carnegie-Mellon University, Pittsburgh, Pa., May 1990.
• 17: ~FEFERMAN, S. Finitary inductively presented logics, In Logic Colloqttilon, '88 (Amsterdam, ~The Netherlands). North Holland, Amsterdam, The Netherlands, 1989, pp. 191-220.
• 18: Amy P. Felty , Dale Miller, Specifying and implementing theorem provers in a higher-order logic programming language, 1989
• 19: ~GORDON, M., MILNER, R., AND WADSWORTH, C. Edinburgh LCF: A Mechanized Logic of ~Computation. In Lecture Notes in Computer Science, vol. 78, Springer-Verlag, New York, ~1979.
• 20: Timothy G. Griffin, An Environment for Formal Systems, Cornell University, Ithaca, NY, 1987
• 21: ~HARPER, R. An equational formulation of LF. Tech. Rep. ECS-LFCS-88-67. Laboratory for ~the Foundations of Computer Science, Edinburgh University, Edinburgh, Scotland, Oct. 1988.
• 22: ~HARPER, R. Systems of polymorphic type assignment in LF. Tech. Rep. CMU-CS-90-144. ~School of Computer Science, Carnegie-Mellon University, Pittsburgh, Pa., June 1990.
• 23: ~HOWARD, W.A. The formulas-as-types notion of construction. In To H, B. Cuny: Essays in ~Combinatory Logic, Lambda Calculus and Folrnalism. Academic Press, Orlando, Fla., 1980, pp. ~479-490.{
• 24: ~HUET, G.P. Unification for typed lambda calculus. Theoret. Comput. Sci. 1, 1 (June 1975), ~27-58.
• 25: Gérard Huet , Gordon Plotkin, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 26: ~JUTnNG, L.S. Checking Landau's grundlagen in the AUTOMATH system. Ph.D. disserta- ~tion. Eindhoven Univ., Eindhoven, The Netherlands, 1977.
• 27: ~MARTIN-EbF, P. About models for intuitionistic type theories and the notion of definitional ~equality. In Proceedings of the 3rd Scandmat'ian Logic Symposium, S. Kange, Ed., Studies in ~Logic and the Foundations of Mathematics, North-Holland, Amsterdam, The Netherlands, ~1975, pp. 81-109.
• 28: ~MART~N-EbF, P. An intuitionistic theory of types: Predicative part. In Logic Colloquium '73 ~H. E. Rose and J. C. Shepherdson, Eds. Studies in Logic and the Foundations of Mathemat- ~ics, vol. 80. North-Holland, Amsterdam, The Netherlands, 1975, pp. 73-118.
• 29: ~MARTIN-EUF, P. Constructive mathematics and computer programming. In Proceedings of ~the 6th International Congress for Logic, Methodology, and Philosophy of Science. North-Hol- ~land, Amsterdam, The Netherlands, pp.153-175.
• 30: ~MARTIN-EbF, P. On the meanings of the logical constants and the justifications of the ~logical laws. Tech. Rep. 2, Scuola di Specializzazione in Logica Matematica. Dipartimento di ~Matematica, Universih di Siena, Sienna, Italy.
• 31: ~MARTIN-EOF, P. Truth of a proposition, evidence of a judgment, validity of a proof. Lecture ~given at the workshop. Theortes of Meaning, Florence, Italy, June 1985 (Available from P. ~Martin-Ebf).
• 32: ~MENDLER, P. F., AND ACZEL, P. The notion of a framework and a framework for LTC. In ~Proceedings of the 3rd Symposium on Logic in Computer Science (Edinburgh, Scotland, July) ~IEEE, New York, 1988, pp. 392-401.
• 33: Albert R. Meyer , Mark B. Reinhold, "Type" is not a type, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.287-295, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512671]
• 34: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 35: John C. Mitchell, Type systems for programming languages, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 36: ~NORSTP(OM, B., PETERSSON, K., AND SMITH, J, M. Programming m Martm-Ebf's type theory: ~An mtroductton. In International Series of Monographs on Computer Science, vol. 7. Oxford ~University Press, Oxford, England, 1990.
• 37: ~PAULSON, m. Interactive theorem proving with Cambridge LCF. Tech. Rep. 80, Computer ~Laboratory, Univ. Cambridge, Cambridge, Mass., Nov. 1985.
• 38: L C Paulson, Natural deduction as higher-order resolution, Journal of Logic Programming, v.3 n.3, p.237-258, Oct. 1986 [doi>10.1016/0743-1066(86)90015-4]
• 39: ~PAULSON, L. The foundations of a generic theorem prover. Tech. Rep. 130, Computer ~Laboratory, Umv. Cambridge, Cambridge, Mass., 1987.
• 40: ~PETERSSON, K. A programming system for type theory. Tech. Rep. 21, Programming ~Methodology Group, Univ. Goteborg/Chalmers Institute of Technology, Goteborg, Sweden, ~Mar. 1982.
• 41: Frank Pfenning, Logic programming in the LF logical framework, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 42: ~PLOTKIN, G. Call-by-name, call-by-value, and the iambda calculus. Theoret. Comput. Scz. l ~(1975), 125-159.
• 43: ~PRAWlTZ, D. Natural Deduction: A Proof-Theoreacal Study. Almquist & Wiksell, Stockhohm ~Sweden, 1965.
• 44: ~PYM, D. Proofs, search and computation m general logic Ph D. dissertation. Edinburgh ~University, Edinburgh, Scotland, 1990. Available as Edinburgh University Computer Science ~Department Technical Report ECS-LFCS-90-125.
• 45: David Pym , Lincoln Wallen, Proof-search in the &lgr;II-calculus, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 46: ~REPS, T. W., AND TEITELBAUM, T. The synthesizer generator reference manual. Tech. Rep., ~Cornell University, Ithaca, N.Y., 1987.
• 47: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 48: ~SALVESEN, A. A proof of the Church-Rosser property for the Edingbugh LF with ,/-conver- ~sion. Lecture given at the First Workshop on Logical Frameworks, Sophia-Antipolis, France, ~May 1990.
• 49: ~SCHOENFIELD, J.R. Mathematical Logic. Addison-Wesley, Reading, Mass., 1967.
• 50: ~SCHP(i3DER-HEISTER, P. A natural extension of natural deduction. J. S),mb. Logic 49, 4 (Dec. ~1984), 1284-1300.
• 51: ~ScldtJYrE, K. Proof Theoo'. Springer-Verlag, New York, 1977.
• 52: ~SELDIN, J. P., AND HINDLEY, J. R., EDS. To H. B, Cure': Essays in CombinatoO, Logic, ~Lambda Calculus and Fbnnahsm. Academic Press, Orlando, Fla., 1980
• 53: ~STENLUND, S. Combinators, A-terms and Proof Theoo,, D. Reidel, Dordrecht, Holland, 1972.
• 54: ~TAKEUTI, G. Proof Theoo'. North-Holland, New York, 1975.
• 55: ~VAN DAALEN, D. T. Thc language theory of AUTOMATH. Ph.D dissertation. Technical ~University of Eindhoven, Eindhoven, The Netherlands, 19811.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Algorithms, Theory, Verification

Keywords:
formal systems, interactive theorem proving, proof checking, typed lambda calculus