Refinement by interpretation in {\pi}-institutions
C\'esar Rodrigues (DI-CCTC, Minho University), Manuel A. Martins (Dep., Mathematics, Aveiro University), Alexandre Madeira (DI-CCTC, Minho, University, Dep. Mathematics, Aveiro University, Critical Software, SA),, Luis S. Barbosa (DI-CCTC, Minho University)
TL;DR
This paper explores how interpretations serve as refinement witnesses within pi-institutions, generalizing previous approaches and establishing a foundation for a refinement calculus of structured specifications across various pi-institutions.
Contribution
It introduces a generalized approach to refinement-by-interpretation in pi-institutions and develops a basis for a refinement calculus applicable to structured specifications.
Findings
Interpretations as multifunctions preserve and reflect logical consequence.
Generalization of refinement-by-interpretation approach.
Foundation for a refinement calculus in pi-institutions.
Abstract
The paper discusses the role of interpretations, understood as multifunctions that preserve and reflect logical consequence, as refinement witnesses in the general setting of pi-institutions. This leads to a smooth generalization of the refinement-by-interpretation approach, recently introduced by the authors in more specific contexts. As a second, yet related contribution a basis is provided to build up a refinement calculus of structured specifications in and across arbitrary pi-institutions.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.