Bidirectional transformations with deltas: A dependently typed approach (talk proposal)

James McKinna*

*Corresponding author for this work

Research output: Contribution to journalConference articlepeer-review

3 Citations (Scopus)


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 languageEnglish
Pages (from-to)32-34
Number of pages3
JournalCEUR Workshop Proceedings
Publication statusPublished - 29 Mar 2016
Event5th International Workshop on Bidirectional Transformations 2016 - Eindhoven, Netherlands
Duration: 8 Apr 20168 Apr 2016

ASJC Scopus subject areas

  • Computer Science(all)


Dive into the research topics of 'Bidirectional transformations with deltas: A dependently typed approach (talk proposal)'. Together they form a unique fingerprint.

Cite this