Skip to main content
SpringerLink
Log in

A Proof Theoretic Interpretation of Model Theoretic Hiding

  • Conference paper
Recent Trends in Algebraic Development Techniques (WADT 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7137))

Included in the following conference series:

Abstract

Logical frameworks like LF are used for formal representations of logics in order to make them amenable to formal machine-assisted meta-reasoning. While the focus has originally been on logics with a proof theoretic semantics, we have recently shown how to define model theoretic logics in LF as well. We have used this to define new institutions in the Heterogeneous Tool Set in a purely declarative way.

It is desirable to extend this model theoretic representation of logics to the level of structured specifications. Here a particular challenge among structured specification building operations is hiding, which restricts a specification to some export interface. Specification languages like ASL and CASL support hiding, using an institution-independent model theoretic semantics abstracting from the details of the underlying logical system.

Logical frameworks like LF have also been equipped with structuring languages. However, their proof theoretic nature leads them to a theory-level semantics without support for hiding. In the present work, we show how to resolve this difficulty.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping 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.

References

  1. 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)

    Chapter  Google Scholar 

  2. Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B.: Algebraic Foundations of Systems Specification. Springer, Heidelberg (1999)

    Book  MATH  Google Scholar 

  3. Barendregt, H.: Lambda calculi with types. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol. 2, Oxford University Press (1992)

    Google Scholar 

  4. Burstall, R., Goguen, J.: The semantics of Clear, a specification language. In: Bjorner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 292–332. Springer, Heidelberg (1980)

    Chapter  Google Scholar 

  5. Bergstra, J.A., Heering, J., Klint, P.: Module algebra. J. ACM 37(2), 335–372 (1990)

    Article  MATH  Google Scholar 

  6. Borzyszkowski, T.: Logical systems for structured specifications. Theor. Comput. Sci. 286(2), 197–245 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  7. Codescu, M., Horozal, F., Kohlhase, M., Mossakowski, T., Rabe, F., Sojakova, K.: Towards Logical Frameworks in the Heterogeneous Tool Set Hets. In: Workshop on Abstract Development Techniques (2010)

    Google Scholar 

  8. Goguen, J., Burstall, R.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39(1), 95–146 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  9. Goguen, J., Rosu, G.: Composing Hidden Information Modules over Inclusive Institutions. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From Object-Orientation to Formal Methods. LNCS, vol. 2635, pp. 96–123. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  10. Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery 40(1), 143–184 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  11. 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

  12. Harper, R., Sannella, D., Tarlecki, A.: Structured presentations and logic representations. Annals of Pure and Applied Logic 67, 113–160 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  13. 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

  14. Kohlhase, M., Mossakowski, T., Rabe, F.: The LATIN Project (2009), https://trac.omdoc.org/LATIN/

  15. Kohlhase, M.: OMDoc – An Open Markup Format for Mathematical Documents (version 1.2). LNCS (LNAI), vol. 4180. Springer, Heidelberg (2006)

    Book  Google Scholar 

  16. Kahrs, S., Sannella, D., Tarlecki, A.: The definition of extended ML: A gentle introduction. Theoretical Computer Science 173(2), 445–484 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  17. Mossakowski, T., Autexier, S., Hutter, D.: Development graphs - Proof management for structured specifications. J. Log. Algebr. Program. 67(1-2), 114–145 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  18. Martin-Löf, P.: An Intuitionistic Theory of Types: Predicative Part. In: Proceedings of the 1973 Logic Colloquium, pp. 73–118. North-Holland (1974)

    Google Scholar 

  19. 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)

    Chapter  Google Scholar 

  20. Mosses, P.D. (ed.): Casl Reference Manual. LNCS, vol. 2960. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  21. Mossakowski, T., Tarlecki, A.: Heterogeneous Logical Environments for Distributed Specifications. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 266–289. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  22. Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)

    Book  MATH  Google Scholar 

  23. 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

  24. Rabe, F., Kohlhase, M.: A Scalable Module System (2010), http://kwarc.info/frabe/Research/mmt.pdf

  25. 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)

    Google Scholar 

  26. Sannella, D., Tarlecki, A.: Specifications in an arbitrary institution. Information and Computation 76, 165–210 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  27. Sannella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Program Development. Springer, Heidelberg (2011)

    MATH  Google Scholar 

  28. Sannella, D., Wirsing, M.: A kernel language for algebraic specification and implementation. In: ADT (1983)

    Google Scholar 

  29. Wirsing, M.: Structured algebraic specifications: A kernel language. Theor. Comput. Sci. 42, 123–249 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  30. Zholudev, V., Kohlhase, M.: TNTBase: a Versioned Storage for XML. In: Proceedings of Balisage: The Markup Conference 2009. Balisage Series on Markup Technologies, vol. 3. Mulberry Technologies, Inc. (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DFKI, Bremen, Germany

    Mihai Codescu & Till Mossakowski

  2. Jacobs University, Bremen, Germany

    Fulya Horozal, Michael Kohlhase & Florian Rabe

Authors
  1. Mihai Codescu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fulya Horozal
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Michael Kohlhase
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Till Mossakowski
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Florian Rabe
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. DFKI, Cyber-Physical Systems, Deutsches Forschungszentrum für künstliche Intelligenz, 28359, Bremen, Germany

    Till Mossakowski

  2. Mathematik und Informatik, Universität Bremen, 28359, Bremen, Germany

    Hans-Jörg Kreowski

Rights and permissions

Reprints 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. (2012). A Proof Theoretic Interpretation of Model Theoretic Hiding. 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_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-28412-0_9

  • 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)

Publish with us

Policies and ethics

Search

Navigation