Formalizing Semantic Bidirectionalization with Dependent Types

Authors: H. Grohne, A. Löh, and J. Voigtländer
Published: In Third International Workshop on Bidirectional Transformations (BX'14, acceptance rate 9/17), an EDBT/ICDT workshop, Athens, Greece, Proceedings, pages 75-81, volume 1133 of CEUR Workshop Proceedings, March 2014.
BibTeX: GLV14.bib
Abstract: Bidirectionalization is the task of automatically inferring one of two transformations that as a pair realize the forward and backward relationship between two domains, subject to certain consistency conditions. A specific technique, semantic bidirectionalization, has been developed that takes a get-function (mapping forwards from sources to views) as input -- but does not inspect its syntactic definition -- and constructs a put-function (mapping an original source and an updated view back to an updated source), guaranteeing standard well-behavedness conditions. Proofs of the latter have been done by hand in the original paper, and recently published extensions of the technique have also come with more or less rigorous proofs or sketches thereof.

In this paper we report on a formalization of the original technique in a dependently typed programming language (turned proof assistant). This yields a complete correctness proof, with no details left out. Besides demonstrating the viability of such a completely formal approach to bidirectionalization, we see further benefits:

  1. Exploration of variations of the original technique could use our formalization as a base line, providing assurance about preservation of the well-behavedness properties as one makes adjustments.
  2. Thanks to being presented in a very expressive type theory, the formalization itself already provides more information about the base technique than the original work. Specifically, while the original by-hand proofs established only a partial correctness result, useful preconditions for total correctness come out of the mechanized formalization.
  3. Finally, also thanks to the very precise types, there is potential for generally improving the bidirectionalization technique itself. Particularly, shape-changing updates are known to be problematic for semantic bidirectionalization, but a refined technique could leverage the information about the relationship between the shapes of sources and views now being expressed at the type level, in a way we very briefly sketch and plan to explore further.
Download: FormalizingSemanticBidirectionalizationWithDependentTypes.pdf
Rights: Copyright held by the authors. Distribution permitted under the terms of the Creative Commons license CC-by-nc-nd 4.0.