Abstract
In recent years in the bx literature, attention has turned to incorporating intensional information about edits (based on monoid actions [HPW12,AU14, for example]), or more generally, deltas (based on categories [DXC11a,DXC+11b]), describing model updates. This talk sketches a dependently-typed approach to consistency maintenance, à la Meertens/Stevens [Mee98, Ste10], building on a propositions-as-types account of consistency [McK16]. The resulting definition of dependently-typed bx (dtbx) has identities and is closed under composition; examples include the above instances of delta-based bx. The definition is "pre-categorical", relying on no ambient assumptions about categorical structure on model spaces. We reconcile the dependently-typed approach to deltas with the categorical by examining analogues of the hippocraticness and overwriteability properties, and discuss this relationship in the context of recent developments in type theory.
Original language | English |
---|---|
Pages (from-to) | 32-34 |
Number of pages | 3 |
Journal | CEUR Workshop Proceedings |
Volume | 1571 |
Publication status | Published - 29 Mar 2016 |
Event | 5th International Workshop on Bidirectional Transformations 2016 - Eindhoven, Netherlands Duration: 8 Apr 2016 → 8 Apr 2016 |
ASJC Scopus subject areas
- General Computer Science