Abstract
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.
This work was supported by Kennedy Carter Ltd and the Engineering and Physical Sciences Research Council (EPSRC grant EP/G03012X/1, ”Higher-Order Refinement Techniques for Model Driven Architecture”).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Boronat, A., Meseguer, J.: An algebraic semantics for the MOF. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 377–391. Springer, Heidelberg (2008)
Constable, R., Mendler, N., Howe, D.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs (1986), Updated edition available at http://www.cs.cornell.edu/Info/Projects/NuPrl/book/doc.html
Königs, A., Schürr, A.: Multi-domain integration with MOF and extended triple graph grammars. In: Bezivin, J., Heckel, R. (eds.) Language Engineering for Model-Driven Software Development number 04101 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany (2005)
Martin-Löf, P.: An Intuitionstic Theory of Types: Predicate Part. In: Rose, H.E., Shepherdson, J.C. (eds.) Logic Colloquium. North-Holland, Oxford (1973)
OMG. Meta Object Facility (MOF) Core Specification, Version 2.0. Object Management Group (January 2006)
Poernomo, I.: A type theoretic framework for formal metamodelling. In: Reussner, R., Stafford, J.A., Szyperski, C. (eds.) Architecting Systems with Trustworthy Components. LNCS, vol. 3938, pp. 262–298. Springer, Heidelberg (2006)
Poernomo, I.: Proofs-as-model-transformations. In: Vallecillo, A., Gray, J., Pierantonio, A. (eds.) ICMT 2008. LNCS, vol. 5063, pp. 214–228. Springer, Heidelberg (2008)
Poernomo, I., Crossley, J., Wirsing, M.: Adapting Proofs-as-Programs: The Curry-Howard Protocol. Monographs in computer science. Springer, Heidelberg (2005)
Rivera, J., Vallecillo, A.: Adding behavioural semantics to models. In: The 11th IEEE International EDOC Conference (EDOC 2007), Annapolis, Maryland, USA, October 15-19, pp. 169–180. IEEE Computer Society, Los Alamitos (2007)
Ruscio, D.D., Jouault, F., Kurtev, I., Bézivin, J., Pierantonio, A.: Extending AMMA for supporting dynamic semantics specifications of DSLs. Technical Report 06.02, Laboratoire d’Informatique de Nantes-Atlantique (LINA), Nantes, France (April 2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Poernomo, I., Terrell, J. (2010). Correct-by-Construction Model Transformations from Partially Ordered Specifications in Coq. In: Dong, J.S., Zhu, H. (eds) Formal Methods and Software Engineering. ICFEM 2010. Lecture Notes in Computer Science, vol 6447. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16901-4_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-16901-4_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16900-7
Online ISBN: 978-3-642-16901-4
eBook Packages: Computer ScienceComputer Science (R0)