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