Advertisement

A Theoretical Foundation for Programming Languages Aggregation

  • Ştefan Ciobâcă
  • Dorel Lucanu
  • Vlad Rusu
  • Grigore Roşu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9463)

Abstract

Programming languages should be formally specified in order to reason about programs written in them. We show that, given two formally specified programming languages, it is possible to construct the formal semantics of an aggregated language, in which programs consist of pairs of programs from the initial languages. The construction is based on algebraic techniques and it can be used to reduce relational properties (such as equivalence of programs) to reachability properties (in the aggregated language).

References

  1. 1.
    Alpuente, M., Escobar, S., Meseguer, J., Ojeda, P.: Order-sorted generalization. Electr. Notes Theor. Comput. Sci. 246, 27–38 (2009)CrossRefzbMATHGoogle Scholar
  2. 2.
    Chiriţă, C.E.: An institutional foundation for the k semantic framework. Master’s thesis, University of Bucharest (2014)Google Scholar
  3. 3.
    Chiriţă, C.E., Şerbănuţă, T.F.: An institutional foundation for the k semantic framework. In: 22nd International Workshop Recent Trends in Algebraic Development Techniques, WADT 2014 (in press)Google Scholar
  4. 4.
    Ciobâcă, Ş.: Reducing partial equivalence to partial correctness. In: 2014 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), pp. 164–171, September 2014Google Scholar
  5. 5.
    Ciobâcă, Ş., Lucanu, D., Rusu, V., Roşu, G.: A language-independent proof system for mutual program equivalence. Technical report 14–01, Al. I. Cuza University (2014)Google Scholar
  6. 6.
    Ciobâcă, Ş., Lucanu, D., Rusu, V., Roşu, G.: A language-independent proof system for mutual program equivalence. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 75–90. Springer, Heidelberg (2014) Google Scholar
  7. 7.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L.: All About Maude, A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007) zbMATHGoogle Scholar
  8. 8.
    Ştefănescu, A., Ciobâcă, Ş., Mereuta, R., Moore, B.M., Şerbănută, T.F., Roşu, G.: All-path reachability logic. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 425–440. Springer, Heidelberg (2014) Google Scholar
  9. 9.
    Diaconescu, R.: Institution-Independent Model Theory. Birkhauser, Basel (2008)zbMATHGoogle Scholar
  10. 10.
    Haxthausen, A.E., Nickl, F.: Pushouts of order-sorted algebraic specifications. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 132–147. Springer, Heidelberg (1996) CrossRefGoogle Scholar
  11. 11.
    Roşu, G., Ellison, C., Schulte, W.: Matching logic: an alternative to Hoare/Floyd logic. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 142–162. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  12. 12.
    Roşu, G.: Matching logic: a logic for structural reasoning. Technical report, University of Illinois, January 2014. http://hdl.handle.net/2142/47004
  13. 13.
    Roşu, G.: Matching logic (invited talk). In: 26th International Conference on Rewriting Techniques and Applications, RTA 2015, 29 June - 1 July, Warsaw, Poland (2015, to appear)Google Scholar
  14. 14.
    Roşu, G., Ştefanescu, A., Ştefan Ciobâcă, Moore, B.M.: One-path reachability logic. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, 25–28 June 2013, New Orleans, LA, USA, pp. 358–367 (2013). http://dx.doi.org/10.1109/LICS.2013.42
  15. 15.
    Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. J. Log. Algebr. Program. 79(6), 397–434 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Sannella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2012). http://dx.doi.org/10.1007/978-3-642-17336-3CrossRefzbMATHGoogle Scholar
  17. 17.
    Schröder, L., Mossakowski, T., Tarlecki, A., Hoffman, P., Klin, B.: Amalgamation in the semantics of CASL. Theoret. Comput. Sci. 331(1), 215–247 (2005). http://dx.doi.org/10.1016/j.tcs.2004.09.037MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Şerbănuţă, T.F., Roşu, G., Meseguer, J.: A rewriting logic approach to operational semantics. Inf. Comput. 207(2), 305–340 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Winskel, G., Nielsen, M.: Categories in concurrency. In: Pitts, A.M., Dybjer, P. (eds.) Semantics and Logics of Computation, Publications of the Newton Institute, pp. 299–354. Cambridge University Press, Cambridge (1997)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Open Access This chapter is distributed under the terms of the Creative Commons Attribution Noncommercial License, which permits any noncommercial use, distribution, and reproduction in any medium, provided the original author(s) and source are credited.

Authors and Affiliations

  • Ştefan Ciobâcă
    • 1
  • Dorel Lucanu
    • 1
  • Vlad Rusu
    • 2
  • Grigore Roşu
    • 1
    • 3
  1. 1.“Alexandru Ioan Cuza” UniversityIaşiRomania
  2. 2.Inria LilleVilleneuve-d’ascqFrance
  3. 3.University of Illinois at Urbana-ChampaignChampaignUSA

Personalised recommendations