Abstract
LF is a meta-logical framework that has become a standard tool for representing logics and studying their properties. Its focus is proof theoretic, employing the Curry-Howard isomorphism: propositions are represented as types, and proofs as terms.
Hets is an integration tool for logics, logic translations and provers, with a model theoretic focus, based on the meta-framework of institutions, a formalisation of the notion of logical system.
In this work, we combine these two worlds. The benefit for LF is that logics represented in LF can be (via Hets) easily connected to various interactive and automated theorem provers, model finders, model checkers, and conservativity checkers - thus providing much more efficient proof support than mere proof checking as is done by systems like Twelf. The benefit for Hets is that (via LF) logics become represented formally, and hence trustworthiness of the implementation of logics is increased, and correctness of logic translations can be mechanically verified. Moreover, since logics and logic translations are now represented declaratively, the effort of adding new logics or translations to Hets is greatly reduced.
This work is part of a larger effort of building an atlas of logics and translations used in computer science and mathematics.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P., Sannella, D., Tarlecki, A.: CASL: The Common Algebraic Specification Language. Theoretical Computer Science 286(2), 153–196 (2002)
Avron, A., Honsell, F., Miculan, M., Paravano, C.: Encoding modal logics in logical frameworks. Studia Logica 60(1), 161–208 (1998)
Autexier, S., Hutter, D., Mantel, H., Schairer, A.: Towards an Evolutionary Formal Software-Development Using CASL. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 73–88. Springer, Heidelberg (2000)
Bertot, Y., Castéran, P.: Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)
Bortin, M., Broch Johnsen, E., Lüth, C.: Structured formal development in Isabelle. Nordic Journal of Computing 12, 1–20 (2006)
Constable, R., Allen, S., Bromley, H., Cleaveland, W., Cremer, J., Harper, R., Howe, D., Knoblock, T., Mendler, N., Panangaden, P., Sasaki, J., Smith, S.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall (1986)
Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of Maude. In: Meseguer, J. (ed.) Proceedings of the First International Workshop on Rewriting Logic, vol. 4, pp. 65–89 (1996)
Church, A.: A Formulation of the Simple Theory of Types. Journal of Symbolic Logic 5(1), 56–68 (1940)
Diaconescu, R.: Institution-independent Model Theory. Birkhäuser (2008)
Goguen, J., Burstall, R.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39(1), 95–146 (1992)
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery 40(1), 143–184 (1993)
Horozal, F., Rabe, F.: Representing Model Theory in a Type-Theoretical Logical Framework. Theoretical Computer Science (to appear, 2011), http://kwarc.info/frabe/Research/HR_folsound_10.pdf
Harper, R., Sannella, D., Tarlecki, A.: Structured presentations and logic representations. Annals of Pure and Applied Logic 67, 113–160 (1994)
Iancu, M., Rabe, F.: Formalizing Foundations of Mathematics. Mathematical Structures in Computer Science (to appear, 2011), http://kwarc.info/frabe/Research/IR_foundations_10.pdf
Kohlhase, M., Mossakowski, T., Rabe, F.: The LATIN Project (2009), https://trac.omdoc.org/LATIN/
Mossakowski, T., Autexier, S., Hutter, D.: Development Graphs - Proof Management for Structured Specifications. Journal of Logic and Algebraic Programming 67(1-2), 114–145 (2006)
Meseguer, J.: General logics. In: Ebbinghaus, H.-D., et al. (eds.) Proceedings of Logic Colloquium, 1987, pp. 275–329. North-Holland (1989)
Martin-Löf, P.: An Intuitionistic Theory of Types: Predicative Part. In: Proceedings of the 1973 Logic Colloquium, pp. 73–118. North-Holland (1974)
Mossakowski, T., Maeder, C., Lüttich, K.: The Heterogeneous Tool Set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007)
MartÃ-Oliet, N., Meseguer, J.: General logics and logical frameworks. In: What is a Logical System?, pp. 355–391. Oxford University Press, Inc., New York (1994)
Mossakowski, T.: Heterogeneous Specification and the Heterogeneous Tool Set. Habilitation thesis (2005), http://www.informatik.uni-bremen.de/~till/
Norell, U.: The Agda WiKi (2005), http://wiki.portal.chalmers.se/agda
Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)
Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)
Paulson, L.C., Coen, M.: Zermelo-Fraenkel Set Theory. Isabelle distribution, ZF/ZF.thy (1993)
Pfenning, F.: Structural cut elimination: I. intuitionistic and classical logic. Information and Computation 157(1-2), 84–141 (2000)
Pfenning, F., Schürmann, C.: System Description: Twelf - A Meta-Logical Framework for Deductive Systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)
Poswolsky, A., Schürmann, C.: System Description: Delphin - A Functional Programming Language for Deductive Systems. In: Abel, A., Urban, C. (eds.) International Workshop on Logical Frameworks and Metalanguages: Theory and Practice. ENTCS, pp. 135–141 (2008)
Pfenning, F., Schürmann, C., Kohlhase, M., Shankar, N., Owre, S.: The Logosphere Project (2003), http://www.logosphere.org/
Rabe, F.: Representing Logics and Logic Translations. PhD thesis, Jacobs University Bremen (2008), http://kwarc.info/frabe/Research/phdthesis.pdf
Rabe, F.: A Logical Framework Combining Model and Proof Theory. Submitted to Mathematical Structures in Computer Science (2010), http://kwarc.info/frabe/Research/rabe_combining_09.pdf
Rabe, F., Schürmann, C.: A Practical Module System for LF. In: Cheney, J., Felty, A. (eds.) Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP), pp. 40–48. ACM Press (2009)
Sojakova, K.: Mechanically Verifying Logic Translations. Master’s thesis, Jacobs University Bremen (2010)
Schürmann, C., Stehr, M.: An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf. In: 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning (2004)
Trybulec, A., Blair, H.: Computer Assisted Reasoning with MIZAR. In: Joshi, A. (ed.) Proceedings of the 9th International Joint Conference on Artificial Intelligence, pp. 26–28 (1985)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 IFIP International Federation for Information Processing
About this paper
Cite this paper
Codescu, M., Horozal, F., Kohlhase, M., Mossakowski, T., Rabe, F., Sojakova, K. (2012). Towards Logical Frameworks in the Heterogeneous Tool Set Hets. In: Mossakowski, T., Kreowski, HJ. (eds) Recent Trends in Algebraic Development Techniques. WADT 2010. Lecture Notes in Computer Science, vol 7137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28412-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-28412-0_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28411-3
Online ISBN: 978-3-642-28412-0
eBook Packages: Computer ScienceComputer Science (R0)