Skip to Main content Skip to Navigation
Conference papers

Programming Language Aggregation with Applications in Equivalence Checking

Ştefan Ciobâcǎ 1 Dorel Lucanu 2 Vlad Rusu 3 Grigore Rosu 4 
3 DREAMPAL - Dynamic Reconfigurable Massively Parallel Architectures and Languages
Université de Lille, Sciences et Technologies, Inria Lille - Nord Europe, CNRS - Centre National de la Recherche Scientifique
Abstract : We show that, given the operational semantics of two programming languages L and R, it is possible to construct an aggregate language, in which programs consist of pairs of programs from L and respectively R. In the aggregate language, a program P = (PL, PR) takes a step from either PL or PR. The main difficulty is how to aggregate the two languages so that data such as integers or booleans that are common to both languages has the same representation in the aggregate language. The aggregation is based on the pushout theorem, which allows us to construct a model of the aggregate language from models of the initial languages, while making sure that the interpretation of common data such as integers is the same. A main application of the aggregation result is in equivalence checking. It is possible to check for example that two programs PL and PR (written in L and respectively R) compute the same result by checking the partial correctness of the pair (PL,PR) in the aggregate language.
Document type :
Conference papers
Complete list of metadata

Cited literature [5 references]  Display  Hide  Download
Contributor : Mister Dart Connect in order to contact the contributor
Submitted on : Tuesday, June 3, 2014 - 8:59:23 AM
Last modification on : Thursday, January 20, 2022 - 4:14:44 PM
Long-term archiving on: : Wednesday, September 3, 2014 - 11:00:37 AM


Files produced by the author(s)


  • HAL Id : hal-00998930, version 1



Ştefan Ciobâcǎ, Dorel Lucanu, Vlad Rusu, Grigore Rosu. Programming Language Aggregation with Applications in Equivalence Checking. Third International Seminar on Program Verification, Automated Debugging and Symbolic Computation (PAS 2014), Jul 2014, Vienne, Austria. ⟨hal-00998930⟩



Record views


Files downloads