A Theoretical Foundation for Programming Languages Aggregation
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).
- 2.Chiriţă, C.E.: An institutional foundation for the k semantic framework. Master’s thesis, University of Bucharest (2014)Google Scholar
- 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.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.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.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
- 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
- 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.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.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
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.