This paper sketches an approach to the synthesis of provably correct model transformations within the Coq theorem prover, an implementation of Coquand and Huet's Calculus of Inductive Constructions. It extends work done by Poernomo on proofs-as-model-transformations in the related formalism of Martin-Löf predicative Constructive Type Theory. We show how the impredicative theory of Coq, together with its treatment of coinductive types, lends itself to the synthesis of a wider range of model transformations than Poernomo had treated before. We illustrate the practical benefits and potential scalability of our approach by means of a case study taken from industry. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Poernomo, I., & Terrell, J. (2010). Correct-by-construction model transformations from partially ordered specifications in coq. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6447 LNCS, pp. 56–73). https://doi.org/10.1007/978-3-642-16901-4_6
Mendeley helps you to discover research relevant for your work.