SVC - A prototype of a Structure-aware Version Control system

Abstract

This thesis studies the problem of structure-aware revision control, which consists of exploiting the knowledge of the structure of data to improve the quality of version control systems. Formats are firstly described using an EDSL, which distinguishes meta-data from the actual content. From the unique format specification inverse-by-construction parser and printer are derived. The data stored in a file is converted into a heterogeneous rose tree, a generic representation of algebraic data types, used by a diff and diff3 algorithm to respectively detect changes and merge revisions. Lastly the semantics and the properties of the two algorithms are studied with a formal model developed in the Agda proof assistant.