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.
['Ştefan Ciobâcă', 'Dorel Lucanu', 'Vlad Rusu', 'Grigore Rosu']
A Theoretical Foundation for Programming Languages Aggregation