Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Building Structured Theories

(Invited Paper)

  • Conference paper
Relational and Algebraic Methods in Computer Science (RAMICS 2011)

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

  • 748 Accesses

Abstract

We provide a set of syntactic tools for structuring large collections of logical theories. Their use is demonstrated by a formalisation of algebras that are used in describing the semantics of concepts in programming languages, but also of more general systems.

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
$34.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

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.

Similar content being viewed by others

References

  1. Agda, http://wiki.portal.chalmers.se/agda/pmwiki.php

  2. Bauer, F.L., et al.: The Munich Project CIP. LNCS, vol. 183. Springer, Heidelberg (1985)

    Book  MATH  Google Scholar 

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

  4. CoFI (The Common Framework Initiative): CASL Reference Manual. LNCS, vol. 2960 (IFIP Series). Springer, Heidelberg (2004)

    Google Scholar 

  5. Cohen, E.: Separation and Reduction. In: Backhouse, R., Oliveira, J. (eds.) MPC 2000. LNCS, vol. 1837, pp. 45–59. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  6. Dang, H.H., Höfner, P.: Automated Higher-Order Reasoning about Quantales. In: Konev, B., Schmidt, R., Schulz, S. (eds.) Proc. Workshop on Practical Aspects of Automated Reasoning (2010)

    Google Scholar 

  7. Dang, H.H., Höfner, P., Möller, B.: Algebraic Separation Logic. J. Log. Algebr. Program. (forthcoming, 2011)

    Google Scholar 

  8. Desharnais, J., Struth, G.: Modal Semirings Revisited. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol. 5133, pp. 360–387. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  9. Desharnais, J., Möller, B., Struth, G.: Kleene Algebra with Domain. ACM Transactions on Computational Logic 7, 798–833 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  10. Dijkstra, E.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

  11. Dijkstra, E.: Computation Calculus Bridging a Formalization Gap. Sci. Comput. Program. 37, 3–36 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  12. Durán, F., Meseguer, J.: Structured Theories and Institutions. Theoretical Computer Science 309, 357–380 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  13. Ehm, T.: Pointer Kleene Algebra. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, pp. 99–111. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  14. Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification I: Equations and Initial Semantics. EATCS-Monographs in Theor. Comp. Sci., vol. 6. Springer, Heidelberg (1985)

    Book  MATH  Google Scholar 

  15. Foster, S., Struth, G., Weber, T.: Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL. In: de Swart, H. (ed.) RAMiCS 2011. LNCS, vol. 6663, pp. 52–67. Springer, Heidelberg (2011)

    Google Scholar 

  16. Giunchiglia, F., Pecchiari, P., Talcott, C.: Reasoning Theories. J. Autom. Reason. 26, 291–331 (2001)

    Article  MATH  Google Scholar 

  17. Gurney, A., Griffin, T.: Pathfinding Through Congruences. In: de Swart, H. (ed.) RAMiCS 2011. LNCS, vol. 6663, pp. 180–195. Springer, Heidelberg (2011)

    Google Scholar 

  18. Guttmann, W., Möller, B.: Modal design algebra. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 236–256. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  19. Guttmann, W., Möller, B.: Normal design algebra. J. Log. Algebr. Program. 79, 144–173 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  20. Harper, R., Sannella, D., Tarlecki, A.: Structured Theory Presentations and Logic Representations. Ann. Pure Appl. Logic 67, 113–160 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  21. He, J., Hoare, T.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)

    MATH  Google Scholar 

  22. Hoare, T., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene Algebra and its Foundations. J. Log. Algebr. Program. (forthcoming, 2011)

    Google Scholar 

  23. Höfner, P.: Algebraic Reasoning with Prover9, http://www.kleenealgebra.de

  24. Höfner, P., McIver, A.: Towards an Algebra of Routing Tables. In: de Swart, H. (ed.) RAMiCS 2011. LNCS, vol. 6663, pp. 212–229. Springer, Heidelberg (2011)

    Google Scholar 

  25. Höfner, P., Möller, B.: Algebraic Neighbourhood Logic. J. Log. Algebr. Program. 76, 35–59 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  26. Höfner, P., Möller, B.: An Algebra of Hybrid Systems. J. Log. Algebr. Program. 78, 74–97 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  27. Höfner, P., Möller, B.: Fixing Zeno Gaps. Theor. Comp. Sci. (forthcoming, 2011)

    Google Scholar 

  28. Höfner, P., Müller, M., Zeissler, S.: ATPPortal: A User-friendly Web Based Interface for Automated Theorem Provers and for Automatically Generated Proofs. University of Augsburg, Institute of Computer Science, Report TR1010-08, http://opus.bibliothek.uni-augsburg.de/volltexte/2010/1673/

  29. Höfner, P., Struth, G.: Automated Reasoning in Kleene Algebra. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 279–294. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  30. Höfner, P., Struth, G., Sutcliffe, G.: Automated Verification of Refinement Laws. Annals of Mathematics and Artificial Intelligence 35, 35–62 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  31. Hollenberg, M.: An Equational Axiomatization of Dynamic Negation and Relational Composition. Journal of Logic, Language and Information 6, 381–401 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  32. Hurd, J.: OpenTheory: Package Management for Higher Order Logic Theories. In: Dos Reis, G., Théry, L. (eds.) PLMMS 2009 — Proc. ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems, pp. 31–37. ACM, New York (2009)

    Google Scholar 

  33. Jones, C.: Development Methods for Computer Programs Including a Notion of Interference. PhD Thesis, University of Oxford. Programming Research Group, Technical Monograph 25 (1981)

    Google Scholar 

  34. Kahl, W.: Collagories — Relation-Algebraic Reasoning for Gluing Constructions. J. Log. Algebr. Program. (forthcoming, 2011)

    Google Scholar 

  35. Kawahara, Y.: On the Cardinality of Relations. In: Schmidt, R. (ed.) RelMiCS/AKA 2006. LNCS, vol. 4136, pp. 251–265. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  36. Kawahara, Y., Winter, M.: Cardinal Addition in Distributive Allegories. In: Berghammer, R., Jaoua, A.M., Möller, B. (eds.) RelMiCS 2009. LNCS, vol. 5827, pp. 227–241. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  37. Kleene, S.: Representation of Events in Nerve Nets and Finite Automata. In: Shannon, C., McCarthy, J. (eds.) Automata Studies, pp. 3–42. Princeton University Press, Princeton (1956)

    Google Scholar 

  38. Kozen, D.: A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Information and Computation 110, 366–390 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  39. Kozen, D.: Kleene Algebra with Tests. Trans. Programming Languages and Systems 19, 427–443 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  40. Luo, Z., Burstall, R.: A Set-theoretic Setting for Structuring Theories in Proof Development. University of Edinburgh, Laboratory for Foundations of Computer Science, Report ECS-LFCS-92-206 (1992)

    Google Scholar 

  41. Manes, E., Benson, D.: The Inverse Semigroup of a Sum-Ordered Semiring. Semigroup Forum 31, 129–152 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  42. McIver, A., Cohen, E., Morgan, C.: Using Probabilistic Kleene Algebra for Protocol Verification. In: Schmidt, R. (ed.) RelMiCS/AKA 2006. LNCS, vol. 4136, pp. 296–310. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  43. Meinicke, L., Solin, K.: Refinement Algebra for Probabilistic Programs. Electr. Notes Theor. Comput. Sci. 201, 177–195 (2008)

    Article  MATH  Google Scholar 

  44. Möller, B.: Kleene Getting Lazy. Sci. Comput. Program. 65, 195–214 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  45. Möller, B., Höfner, P., Struth, G.: Quantales and Temporal Logics. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 263–277. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  46. Möller, B., Struth, G.: Algebras of Modal Operators and Partial Correctness. Theor. Comp. Sci. 351, 221–239 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  47. Möller, B., Struth, G.: wp is wlp. In: MacCaull, W., Winter, M., Düntsch, I. (eds.) RelMiCS 2005. LNCS, vol. 3929, pp. 200–211. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  48. Moszkowski, B.: A Complete Axiomatization of Interval Temporal Logic with Infinite Time. In: LICS 2000, pp. 241–252 (2000)

    Google Scholar 

  49. Mulvey, C.: &. Rendiconti del Circolo Matematico di Palermo 12, 99–104 (1986)

    Google Scholar 

  50. Paulson, L., Nipkow, T., Wenzel, M.: Isabelle, http://www.cl.cam.ac.uk/research/hvg/Isabelle/

  51. Parikh, R.: Propositional Logics of Programs: New Directions. In: Karpinski, M. (ed.) FCT 1983. LNCS, vol. 158, pp. 347–359. Springer, Heidelberg (1983)

    Chapter  Google Scholar 

  52. Pauly, M., Parikh, R.: Game Logic; An Overview. Studia Logica 75, 165–182 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  53. Park, D.: On the Semantics of Fair Parallelism. In: Bjørner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 504–526. Springer, Heidelberg (1980)

    Chapter  Google Scholar 

  54. Reynolds, J.: An Introduction to Separation Logic. In: Broy, M., Sitou, W., Hoare, T. (eds.) Engineering Methods and Tools for Software Safety and Security, pp. 285–310. IOS Press, Amsterdam (2009)

    Google Scholar 

  55. Rosenthal, K.: Quantales and their Applications. Pitman Research Notes in Math, vol. 234. Longman Scientific and Technical (1990)

    Google Scholar 

  56. Sannella, D., Burstall, R.M.: Structured Theories in LCF. In: Ausiello, G., Protasi, M. (eds.) CAAP 1983. LNCS, vol. 159, pp. 377–391. Springer, Heidelberg (1983)

    Chapter  Google Scholar 

  57. Sintzoff, M.: Iterative Synthesis of Control Guards Ensuring Invariance and Inevitability in Discrete-Decision Games. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From Object-Orientation to Formal Methods. LNCS, vol. 2635, pp. 272–301. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  58. Smith, D.: Automating the Design of Algorithms. In: Möller, B., Schuman, S., Partsch, H. (eds.) Formal Program Development. LNCS, vol. 755, pp. 324–354. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  59. Solin, K., von Wright, J.: Enabledness and Termination in Refinement Algebra. Sci. Comput. Program. 74, 654–668 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  60. Specware, http://www.specware.org/

  61. Srinivas, Y., Jüllig, R.: Specware: Formal Support for Composing Software. In: Möller, B. (ed.) MPC 1995. LNCS, vol. 947, pp. 399–422. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  62. Struth, G.: Isabelle Repository for Relational and Algebraic Methods, http://staffwww.dcs.shef.ac.uk/people/G.Struth/isa/

  63. Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. J. Autom. Reas. 43, 337–362 (2009)

    Article  MATH  Google Scholar 

  64. Takai, T., Furusawa, H.: Monadic Tree Kleene Algebra. In: Schmidt, R. (ed.) RelMiCS/AKA 2006. LNCS, vol. 4136, pp. 402–416. Springer, Heidelberg (2006), http://www.sci.kagoshima-u.ac.jp/~furusawa/person/Papers/correct_monodic_kleene_algebra.pdf

    Chapter  Google Scholar 

  65. von Karger, B.: Temporal Algebra. Mathematical Structures in Computer Science 8, 277–320 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  66. von Wright, J.: Towards a Refinement Algebra. Sci. Comput. Program. 51, 23–45 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  67. Wirsing, M.: Structured Algebraic Specifications: A Kernel Language. Theor. Comput. Sci. 42, 123–249 (1986)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Universität Augsburg, D-86135, Augsburg, Germany

    Bernhard Möller

Authors
  1. Bernhard Möller
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Philosophy, Tilburg University, P.O. Box 90153, 5000, Tilburg, LE, The Netherlands

    Harrie de Swart

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Möller, B. (2011). Building Structured Theories. In: de Swart, H. (eds) Relational and Algebraic Methods in Computer Science. RAMICS 2011. Lecture Notes in Computer Science, vol 6663. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21070-9_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-21070-9_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-21069-3

  • Online ISBN: 978-3-642-21070-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation