A Type-Theoretic Framework for Certified Model Transformations - Formal Methods: Foundations and Applications - page 115

2.1 The CIC as a Technical Space
The CIC is a type theory, i.e. in brief, a higher order logic in which the individuals
are classified into a hierarchy of types. The types work very much as in strongly
typed functional programming languages which means that, to begin with, there
are basic elementary types, recursive types defined by induction like lists and
trees (called inductive types) and function types. A (dependent) record type is a
non-recursive inductive type with a single constructor and projection functions
for each field of the type. An example of inductive type is given by the following
definition of the lists of elements of (parametric) type A ,whichwegiveinCoq
notation (data types are called “Sets” in the CIC):
Inductive list : Set :=
| nil : list
| cons : A -> list -> list.
The type is defined by its constructors, in this case nil: list A and
cons : A -> list A -> list A and it is understood that its elements are ob-
tained as finite combinations of the constructors. Well-founded recursion for
these types is available via the Fixpoint operator.
On top of this, a higher-order logic is available which serves to predicate on the
various data types. The interpretation of the propositions is constructive, i.e. a
proposition is defined by specifying what a proof of it is and a proposition is true
if and only if a proof of it has been constructed. As a consequence, elementary
predicates are also defined as inductive types, by giving the corresponding proof
constructors. The type of propositions is called Prop .
We refer to [18,12] for further details on the CIC and Coq, respectively.
2.2 The Framework at a Glance
Although our approach is language independent, we are working with the ATL
technical space. ATL (Atlas Transformation Language, [8]) is a hybrid of declar-
ative and imperative transformation language. Since we are concerned with a
model-to-model relational approach, we focused on the declarative part of ATL.
In this context, an ATL transformation specification is composed of rules that
define the correspondence between source and target model elements. In this
technical space, source and target metamodels are specified using KM3 (Kernel
MetaMetaModel, [3]) which provides a textual concrete syntax that eases the
coding of metamodels.
During software construction a developer specifies the input and output meta-
models and the transformation between them. We propose that at this point
a separation of duties is implemented for performing formal verification. We
conceive the participation of a (human, expert) verifier, who will carry out a
semi-automatic translation process from the ATL to the CIC technical space, as
outlined in Figure 2.