The purpose of this project is to explore a variant of hybrid logics in which worlds are equipped with Alloy models. In principle, such a logic (generated via the hybridisation method "hybridisation") provides a canonical language to address reconfigurability in Alloy specifications.
The workplan involves the implementation of a calculus for this logic (reported in Proof theory for hybridised logics) and the development of a case study that illustrates its potentialities (and limitations) in the software development process.