Hostname: page-component-78c5997874-94fs2 Total loading time: 0 Render date: 2024-11-03T00:42:03.593Z Has data issue: false hasContentIssue false
  • English
  • Français

A logical framework combining model and proof theory

Published online by Cambridge University Press:  01 March 2013

FLORIAN RABE
FLORIAN RABE*
Affiliation:
Computer Science, Jacobs University Bremen, Campus Ring 1, 28759 Bremen, Germany Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Mathematical logic and computer science have driven the design of a growing number of logics and related formalisms such as set theories and type theories. In response to this population explosion, logical frameworks have been developed as formal meta-languages in which to represent, structure, relate and reason about logics.

Research on logical frameworks has diverged into separate communities, often with conflicting backgrounds and philosophies. In particular, two of the most important logical frameworks are the framework of institutions, from the area of model theory based on category theory, and the Edinburgh Logical Framework LF, from the area of proof theory based on dependent type theory. Even though their ultimate motivations overlap – for example in applications to software verification – they have fundamentally different perspectives on logic.

In the current paper, we design a logical framework that integrates the frameworks of institutions and LF in a way that combines their complementary advantages while retaining the elegance of each of them. In particular, our framework takes a balanced approach between model theory and proof theory, and permits the representation of logics in a way that comprises all major ingredients of a logic: syntax, models, satisfaction, judgments and proofs. This provides a theoretical basis for the systematic study of logics in a comprehensive logical framework. Our framework has been applied to obtain a large library of structured and machine-verified encodings of logics and logic translations.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 23 , Issue 5 , October 2013 , pp. 945 - 1001
Copyright
Copyright © Cambridge University Press 2013 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Aiguier, M. and Diaconescu, R. (2007) Stratified institutions and elementary homomorphisms. Information Processing Letters 103 (1)5–13.CrossRefGoogle Scholar
Andrews, P. (1986) An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Academic Press.Google Scholar
Avron, A., Honsell, F., Mason, I. and Pollack, R. (1992) Using typed lambda calculus to implement formal systems on a machine. Journal of Automated Reasoning 9 (3)309–354.CrossRefGoogle Scholar
Avron, A., Honsell, F., Miculan, M. and Paravano, C. (1998) Encoding modal logics in logical frameworks. Studia Logica 60 (1)161–208.CrossRefGoogle Scholar
Awodey, S. and Rabe, F. (2011) Kripke Semantics for Martin-Löf's Extensional Type Theory. Logical Methods in Computer Science 7 (3).Google Scholar
Baader, F., Calvanese, D., McGuinness, D., Nardi, D. and Patel-Schneider, P. (eds.) (2003) The Description Logic Handbook: Theory, Implementation and Applications, Cambridge University Press.Google Scholar
Barendregt, H. (1992) Lambda calculi with types. In: Abramsky, S., Gabbay, D. and Maibaum, T. (eds.) Handbook of Logic in Computer Science, volume 2, Oxford University Press.Google Scholar
Barwise, J. (1977) An Introduction to First-Order Logic. In: Barwise, J. (ed.) Handbook of Mathematical Logic, North-Holland5–46.CrossRefGoogle Scholar
Benton, N., Kennedy, A. and Varming, C. (2009) Some Domain Theory and Denotational Semantics in Coq. In: Berghofer, S., Nipkow, T., Urban, C. and Wenzel, M. (eds.) Theorem Proving in Higher Order Logics. Springer-Verlag Lecture Notes in Computer Science 5674 115–130.CrossRefGoogle Scholar
Benzmüller, C., Paulson, L., Theiss, F. and Fietzke, A. (2008) LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). In: Armando, A., Baumgartner, P. and Dowek, G. (eds.) Automated Reasoning – 5th International Joint Conference, IJCAR 2010. Springer-Verlag Lecture Notes in Computer Science 6173 162–170.CrossRefGoogle Scholar
Bertot, Y. and Castéran, P. (2004) Coq'Art: The Calculus of Inductive Constructions, Springer-Verlag.Google Scholar
Béziau, J. (ed.) (2005) Logica Universalis, Birkhäuser.CrossRefGoogle Scholar
Borzyszkowski, T. (2000) Higher-Order Logic and Theorem Proving for Structured Specifications. In: Choppy, C., Bert, D. and Mosses, P. (eds.) Workshop on Algebraic Development Techniques. Springer-Verlag Lecture Notes in Computer Science 1827 401–418.CrossRefGoogle Scholar
Bourbaki, N. (1974) Algebra I, Elements of Mathematics, Springer-Verlag.Google Scholar
Brachman, R. and Schmolze, J. (1985) An Overview of the KL-ONE Knowledge Representation Scheme. Cognitive Science 9 (2).Google Scholar
Brouwer, L. (1907) Over de grondslagen der wiskunde, Ph.D. thesis, Universiteit van Amsterdam. (English title: On the Foundations of Mathematics.)Google Scholar
Cartmell, J. (1986) Generalized algebraic theories and contextual category. Annals of Pure and Applied Logic 32 209–243.CrossRefGoogle Scholar
Căzănescu, V. and Roşu, G. (1997) Weak inclusion systems. Mathematical Structures in Computer Science 7 (2)195–206.CrossRefGoogle Scholar
Cerioli, M. and Meseguer, J. (1997) May I Borrow Your Logic? (Transporting Logical Structures along Maps). Theoretical Computer Science 173 311–347.CrossRefGoogle Scholar
Cervesato, I. and Pfenning, F. (2002) A Linear Logical Framework. Information and Computation 179 (1)19–75.CrossRefGoogle Scholar
Church, A. (1940) A Formulation of the Simple Theory of Types. Journal of Symbolic Logic 5 (1)56–68.CrossRefGoogle Scholar
Clavel, M., Eker, S., Lincoln, P. and Meseguer, J. (1996) Principles of Maude. In: Meseguer, J. (ed.) Proceedings of the First International Workshop on Rewriting Logic. Electronic Notes in Theoretical Computer Science 4 65–89.CrossRefGoogle Scholar
Codescu, M., Horozal, F., Kohlhase, M., Mossakowski, T. and Rabe, F. (2011) Project Abstract: Logic Atlas and Integrator (LATIN). In: Davenport, J., Farmer, W., Rabe, F. and Urban, J. (eds.) Intelligent Computer Mathematics. Springer-Verlag Lecture Notes in Computer Science 6824 287–289.Google Scholar
Codescu, M., Horozal, F., Kohlhase, M., Mossakowski, T., Rabe, F. and Sojakova, K. (2012) Towards Logical Frameworks in the Heterogeneous Tool Set Hets. In: Mossakowski, T. and Kreowski, H. (eds.) Recent Trends in Algebraic Development Techniques 2010. Springer-Verlag Lecture Notes in Computer Science 7137 139–159.CrossRefGoogle Scholar
Coquand, T. and Dybjer, P. (1997) Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science 7 (1)75–94.CrossRefGoogle Scholar
Coquand, T. and Huet, G. (1988) The Calculus of Constructions. Information and Computation 76 (2/3)95–120.CrossRefGoogle Scholar
Curry, H. and Feys, R. (1958) Combinatory Logic, North-Holland.Google Scholar
de Bruijn, N. (1970) The Mathematical Language AUTOMATH. In: Laudet, M. (ed.) Proceedings of the Symposium on Automated Demonstration. Springer-Verlag Lecture Notes in Mathematics 25 29–61.CrossRefGoogle Scholar
de Bruijn, N. (1991) A Plea for Weaker Frameworks. In: Huet, G. and Plotkin, G. (eds.) Logical Frameworks, Cambridge University Press 40–67.CrossRefGoogle Scholar
Diaconescu, R. (2002) Grothendieck institutions. Applied Categorical Structures 10 (4)383–402.CrossRefGoogle Scholar
Diaconescu, R. (2006) Proof systems for institutional logic. Journal of Logic and Computation 16 (3)339–357.CrossRefGoogle Scholar
Diaconescu, R. (2008) Institution-independent Model Theory, Birkhäuser.Google Scholar
Dumbrava, S. and Rabe, F. (2010) Structuring Theories with Partial Morphisms. In: Workshop on Algebraic Development Techniques.Google Scholar
Farmer, W. (2010) Chiron: A set theory with types, undefinedness, quotation, and evaluation. SQRL Report 38, McMaster University.Google Scholar
Farmer, W., Guttman, J. and Thayer, F. (1992) Little Theories. In: Kapur, D. (ed.) International Conference on Automated Deduction (CADE). Springer-Verlag Lecture Notes in Computer Science 607 567–581.CrossRefGoogle Scholar
Fiadeiro, J. and Sernadas, A. (1988) Structuring theories on consequence. In: Recent Trends in Data Type Specification. Springer-Verlag Lecture Notes in Computer Science 332 44–72.CrossRefGoogle Scholar
Fraenkel, A. (1922) Zu den Grundlagen der Cantor–Zermeloschen Mengenlehre. Mathematische Annalen 86 230–237. (English title: On the Foundation of Cantor–Zermelo Set Theory.)CrossRefGoogle Scholar
Gentzen, G. (1934) Untersuchungen über das logische Schließen I and II. Mathematische Zeitschrift 39 176–210 and 405–431. (English title: Investigations into Logical Deduction.)CrossRefGoogle Scholar
Girard, J. (1987) Linear Logic. Theoretical Computer Science 50 1–102.CrossRefGoogle Scholar
Gödel, K. (1930) Die Vollständigkeit der Axiome des Logischen Funktionenkalküls. Monatshefte für Mathematik und Physik 37 349–360. (English title: The Completeness of the Axioms of the Logical Calculus of Functions.)CrossRefGoogle Scholar
Goguen, J. and Burstall, R. (1986) A study in the foundations of programming methodology: specifications, institutions, charters and parchments. In: Pitt, D., Abramsky, S., Poigné, A. and Rydeheard, D., (eds.) Workshop on Category Theory and Computer Programming. Springer-Verlag Lecture Notes in Computer Science 240 313–333.CrossRefGoogle Scholar
Goguen, J. and Burstall, R. (1992) Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39 (1)95–146.CrossRefGoogle Scholar
Goguen, J., Mossakowski, T., de Paiva, V., Rabe, F. and Schröder, L. (2007) An Institutional View on Categorical Logic. International Journal of Software and Informatics 1 (1)129–152.Google Scholar
Goguen, J. and Rosu, G. (2002) Institution morphisms. Formal Aspects of Computing 13 274–307.CrossRefGoogle Scholar
Goguen, J., Thatcher, J. and Wagner, E. (1978) An initial algebra approach to the specification, correctness and implementation of abstract data types. In: Yeh, R. (ed.) Current Trends in Programming Methodology, volume 4, Prentice Hall80–149.Google Scholar
Gordon, M. (1988) HOL: A Proof Generating System for Higher-Order Logic. In: Birtwistle, G. and Subrahmanyam, P. (eds.) VLSI Specification, Verification and Synthesis, Kluwer-Academic Publishers 73–128.CrossRefGoogle Scholar
Haftmann, F. and Wenzel, M. (2006) Constructive Type Classes in Isabelle. In: Altenkirch, T. and McBride, C. (eds.) Types for Proofs and Programs: Selected papers, International Workshop, TYPES 2006. Springer-Verlag Lecture Notes in Computer Science 4502 160–174.CrossRefGoogle Scholar
Harper, R., Honsell, F. and Plotkin, G. (1993) A framework for defining logics. Journal of the Association for Computing Machinery 40 (1)143–184.CrossRefGoogle Scholar
Harper, R., Sannella, D. and Tarlecki, A. (1994) Structured presentations and logic representations. Annals of Pure and Applied Logic 67 113–160.CrossRefGoogle Scholar
Harrison, J. (1996) HOL Light: A Tutorial Introduction. In: Srivas, M. K. and Camilleri, A. J. (eds.) Proceedings of the First International Conference on Formal Methods in Computer-Aided Design. Springer-Verlag Lecture Notes in Computer Science 1166 265–269.CrossRefGoogle Scholar
Henkin, L. (1950) Completeness in the Theory of Types. Journal of Symbolic Logic 15 (2)81–91.CrossRefGoogle Scholar
Hilbert, D. (1926) Über das Unendliche. Mathematische Annalen 95 161–90.CrossRefGoogle Scholar
Horozal, F. and Rabe, F. (2011) Representing Model Theory in a Type-Theoretical Logical Framework. Theoretical Computer Science 412 (37)4919–4945.CrossRefGoogle Scholar
Howard, W. (1980) The formulas-as-types notion of construction. In: To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, Academic Press 479–490.Google Scholar
Iancu, M. and Rabe, F. (2011) Formalising Foundations of Mathematics. Mathematical Structures in Computer Science 21 (4)883–911.CrossRefGoogle Scholar
Keller, C. and Werner, B. (2010) Importing HOL Light into Coq. In: Kaufmann, M. and Paulson, L. (eds.) Interactive Theorem Proving. Springer-Verlag Lecture Notes in Computer Science 6172 307–322.CrossRefGoogle Scholar
Kohlhase, M., Rabe, F. and Zholudev, V. (2010) Towards MKM in the Large: Modular Representation and Scalable Software Architecture. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P., Rideau, L., Rioboo, R. and Sexton, A. (eds.) Intelligent Computer Mathematics. Springer-Verlag Lecture Notes in Computer Science 6167 370–384.CrossRefGoogle Scholar
Krauss, A. and Schropp, A. (2010) A Mechanized Translation from Higher-Order Logic to Set Theory. In: Kaufmann, M. and Paulson, L. (eds.) Interactive Theorem Proving. Springer-Verlag Lecture Notes in Computer Science 6172 323–338.CrossRefGoogle Scholar
Lambek, J. and Scott, P. (1986) Introduction to Higher-Order Categorical Logic, Cambridge Studies in Advanced Mathematics 7, Cambridge University Press.Google Scholar
Lawvere, F. (1963) Functional Semantics of Algebraic Theories, Ph.D. thesis, Columbia University.CrossRefGoogle Scholar
Lawvere, W. (1969) Adjointness in Foundations. Dialectica 23 (3–4)281–296.CrossRefGoogle Scholar
MacLane, S. Lane, S. (1998) Categories for the working mathematician, Springer-Verlag.Google Scholar
Martí-Oliet, N. and Meseguer, J. (1996) Rewriting Logic as a Logical and Semantic Framework. In: Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science 4 352–358.Google Scholar
Martin-Löf, P. (1974) An Intuitionistic Theory of Types: Predicative Part. In: Proceedings of the ‘73 Logic Colloquium, North-Holland73–118.Google Scholar
Martin-Löf, P. (1996) On the meanings of the logical constants and the justifications of the logical laws. Nordic Journal of Philosophical Logic 1 (1)3–10.Google Scholar
McLaughlin, S. (2006) An Interpretation of Isabelle/HOL in HOL Light. In: Shankar, N. and Furbach, U. (eds.) Proceedings of the 3rd International Joint Conference on Automated Reasoning. Springer-Verlag Lecture Notes in Computer Science 4130 192–204.CrossRefGoogle Scholar
Meseguer, J. (1989) General logics. In: Ebbinghaus, H.-D.et al. (eds.) Proceedings, Logic Colloquium 1987, North-Holland275–329.Google Scholar
Mossakowski, T. (2005) Heterogeneous Specification and the Heterogeneous Tool Set, Habilitation thesis. (Available at http://www.informatik.uni-bremen.de/till/.)Google Scholar
Mossakowski, T., Goguen, J., Diaconescu, R. and Tarlecki, A. (2005) What is a logic? In: Béziau, J. (ed.) Logica Universalis, Birkhäuser 113–133.CrossRefGoogle Scholar
Mossakowski, T., Maeder, C. and Lüttich, K. (2007) The Heterogeneous Tool Set. In: Grumberg, O. and Huth, M. (ed.) TACAS 2007. Springer-Verlag Lecture Notes in Computer Science 4424 519–522.CrossRefGoogle Scholar
Mossakowski, T., Tarlecki, A. and Pawlowski, W. (1997) Combining and Representing Logical Systems. In: Moggi, E. and Rosolini, G. (eds.) Category Theory and Computer Science 1290 177–196.CrossRefGoogle Scholar
Mosses, P. D. (ed.) (2004) CASL Reference Manual. Springer-Verlag Lecture Notes in Computer Science 2960.CrossRefGoogle Scholar
Naumov, P., Stehr, M. and Meseguer, J. (2001) The HOL/NuPRL proof translator – a practical approach to formal interoperability. In: Boulton, R. and Jackson, P. (eds.) 14th International Conference on Theorem Proving in Higher Order Logics. Springer-Verlag Lecture Notes in Computer Science 2152 329–345.CrossRefGoogle Scholar
Nipkow, T., Paulson, L. and Wenzel, M. (2002) Isabelle/HOL – A Proof Assistant for Higher-Order Logic. Springer-Verlag Lecture Notes in Computer Science 2283.CrossRefGoogle Scholar
Norell, U. (2005) The Agda WiKi. (Available at http://wiki.portal.chalmers.se/agda.)Google Scholar
Obua, S. and Skalberg, S. (2006) Importing HOL into Isabelle/HOL. In: Shankar, N. and Furbach, U. (eds.) Proceedings of the 3rd International Joint Conference on Automated Reasoning. Springer-Verlag Lecture Notes in Computer Science 4130 298–302.CrossRefGoogle Scholar
Owre, S., Rushby, J. and Shankar, N. (1992) PVS: A Prototype Verification System. In: Kapur, D. (ed.) 11th International Conference on Automated Deduction (CADE). Springer-Verlag Lecture Notes in Computer Science 607 748–752.CrossRefGoogle Scholar
Paulson, L. (1994) Isabelle: A Generic Theorem Prover. Springer-Verlag Lecture Notes in Computer Science 828.Google Scholar
Pfenning, F. (2000) Structural cut elimination I: intuitionistic and classical logic. Information and Computation 157 (1–2)84–141.CrossRefGoogle Scholar
Pfenning, F. (2001) Logical frameworks. In: Handbook of automated reasoning, Elsevier 1063–1147.CrossRefGoogle Scholar
Pfenning, F. and Schürmann, C. (1999) System description: Twelf – a meta-logical framework for deductive systems. Springer-Verlag Lecture Notes in Computer Science 1632 202–206.CrossRefGoogle Scholar
Pfenning, F., Schürmann, C., Kohlhase, M., Shankar, N. and Owre, S. (2003) The Logosphere Project. (Available at http://www.logosphere.org/.)Google Scholar
Pientka, B. and Dunfield, J. (2010) A Framework for Programming and Reasoning with Deductive Systems (System description). In: Armando, A., Baumgartner, P. and Dowek, G. (eds.) Automated Reasoning – 5th International Joint Conference, IJCAR 2010. Springer-Verlag Lecture Notes in Computer Science 6173 15–21.CrossRefGoogle Scholar
Pitts, A. (2000) Categorical Logic. In: Abramsky, S., Gabbay, D. and Maibaum, T. (eds.) Handbook of Logic in Computer Science, Volume 5. Algebraic and Logical Structures, Oxford University Press 39–128.Google Scholar
Poswolsky, A. and Schürmann, C. (2008) System Description: Delphin – A Functional Programming Language for Deductive Systems. In: Abel, A. and Urban, C. (eds.) International Workshop on Logical Frameworks and Metalanguages: Theory and Practice. Electronic Notes in Theoretical Computer Science 228 113–120.CrossRefGoogle Scholar
Rabe, F. (2008) Representing Logics and Logic Translations, Ph.D. thesis, Jacobs University Bremen. (Available at http://kwarc.info/frabe/Research/phdthesis.pdf.)Google Scholar
Rabe, F. and Kohlhase, M. (2011) A Scalable Module System. (Available at http://arxiv.org/abs/1105.0548.)Google Scholar
Rabe, F. and Schürmann, C. (2009) A Practical Module System for LF. In: Cheney, J. and Felty, A. (eds.) Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP), ACM International Conference Proceedings Series, LFMTP'09 40–48.Google Scholar
Robinson, A. (1950) On the application of symbolic logic to algebra. In: Proceedings of the International Congress of Mathematicians, American Mathematical Society 686–694.Google Scholar
Seely, R. (1984) Locally cartesian closed categories and type theory. Mathematical Proceedings of the Cambridge Philosophical Society 95 33–48.CrossRefGoogle Scholar
Smullyan, R. (1995) First-Order Logic (second corrected edition), Dover.Google Scholar
Sojakova, K. (2010) Mechanically Verifying Logic Translations, Master's thesis, Jacobs University Bremen.Google Scholar
Tarlecki, A. (1996) Moving between logical systems. In: Haveraaen, M., Owe, O. and Dahl, O.-J. (eds.) Recent Trends in Data Type Specifications – 11th Workshop on Specification of Abstract Data Types. Springer-Verlag Lecture Notes in Computer Science 1130 478–502.CrossRefGoogle Scholar
Tarski, A. (1933) Pojȩcie prawdy w jȩzykach nauk dedukcyjnych. Prace Towarzystwa Naukowego Warszawskiego Wydzial III Nauk Matematyczno-Fizycznych 34. (English title: The concept of truth in the languages of the deductive sciences.)Google Scholar
Tarski, A. and Vaught, R. (1956) Arithmetical extensions of relational systems. Compositio Mathematica 13 81–102.Google Scholar
Trybulec, A. and Blair, H. (1985) Computer Assisted Reasoning with MIZAR. In: Joshi, A. (ed.) Proceedings of the 9th International Joint Conference on Artificial Intelligence 26–28.Google Scholar
Whitehead, A. and Russell, B. (1913) Principia Mathematica, Cambridge University Press.Google Scholar
Zermelo, E. (1908) Untersuchungen über die Grundlagen der Mengenlehre I. Mathematische Annalen 65 261–281. (English title: Investigations in the foundations of set theory I.)CrossRefGoogle Scholar