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.
|Number of pages||3|
|Journal||CEUR Workshop Proceedings|
|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
- Computer Science(all)