Y. Bertot & P. Castéran (2004):
Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions.
Texts in Theoretical Computer Science.
Springer-Verlag,
doi:10.1007/978-3-662-07964-5.
A. Boronat & J. Mesegeur (2008):
An Algebraic Semantics for the MOF.
In: J. Fiadeiro & P. Inverardi: FASE 2008 Proceedings,
LNCS 4961.
Springer,
pp. 377–391,
doi:10.1007/978-3-540-78743-3_28.
Daniel Calegari, Carlos Luna, Nora Szasz & Alvaro Tasistro (2011):
A Type-Theoretic Framework for Certified Model Transformations.
In: Jim Davies, Leila Silva & Adenilso da Silva Simão: Formal Methods: Foundations and Applications - 13th Brazilian Symposium on Formal Methods, SBMF 2010, Natal, Brazil, November 8-11, 2010, Revised Selected Papers,
Lecture Notes in Computer Science 6527.
Springer,
pp. 112–127,
doi:10.1007/978-3-642-19829-8_8.
M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer & C. Talcott (2003):
The Maude 2.0 System.
In: Rewriting Techniques and Applications (RTA 2003),
Lecture Notes in Computer Science 2706.
Springer-Verlag,
pp. 76–87,
doi:10.1007/3-540-44881-0_7.
H.B. Curry & R. Feys (1958):
Combinatory Logic 1.
North Holland Publishing Company.
Object Management Group (2003):
MDA Guide Version 1.0.1.
Object Management Group (2009):
Unified Modelling Language, Version 2.2.
Formal/09-02-02, formal/09-02-04.
Object Management Group (2011):
Meta Object Facility (MOF) 2.0 Query/View/Transformation Specification.
Formal/2011-01-01.
W.A. Howard (1980):
The Formulae-as-Types Notion of Construction.
In: J.P. Seldin & J.R. Hindley: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism.
Academic Press Inc.
F. Jouault & I. Kurtev (2006):
Transforming Models with ATL.
LNCS 3844.
MODELS 2005 Workshops.
Springer-Verlag,
pp. 128–138,
doi:10.1007/11663430_14.
K. Lano (2009):
Model-Driven Software Development with UML and JAVA.
Cengage Learning EMEA.
P. Martin-Löf (1984):
Intuitionistic Type Theory.
Bibliopolis.
S.J. Mellor, K. Scott, A. Uhl & D. Weise (2004):
MDA Distilled.
Addison-Wesley.
Object Management Group (2006):
Meta Object Facility (MOF) Core Specification.
Formal/06-01-01.
Object Management Group (2012):
Object Constraint Language (OCL), Version 2.3.1.
Formal/2012-01-01.
I.H. Poernomo (2008):
Proofs-as-Model-Transformations.
In: Antonio Vallecillo, Jeff Gray & Alfonso Pierantonio: Theory and Practice of Model Transformations, First International Conference, ICMT 2008, Zürich, Switzerland, July 1-2, 2008, Proceedings,
Lecture Notes in Computer Science 5063.
Springer,
pp. 214–228,
doi:10.1007/978-3-540-69927-9_15.
I.H. Poernomo & J.W. Terrell (2010):
Correct-by-Construction Model Transformations from Partially Ordered Specifications.
In: J.S. Dong & H. Zhu: Formal Methods and Software Engineering,
Lecture Notes in Computer Science 6447.
12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19.
Springer,
doi:10.1007/978-3-642-16901-4_6.
J. Rivera & A. Vallecillo (2007):
Adding Behavioural Semantics to Models.
In: The 11th IEEE International EDOC Conference (EDOC 2007).
IEEE Computer Society,
Annapolis, Maryland, USA,
pp. 169–180.
D. Ruscio, F. Jouault, I. Kurtev, J. Beżivin & A. Pierantonio (2006):
Extending AMMA for Supporting Dynamic Semantics Specifications of DSLs.
Technical Report 06.02.
Laboratoire d'Informatique de Nantes-Atlantique (LINA),
Nantes, France.
S. Shlaer & S.J. Mellor (1988):
Object-Oriented Systems Analysis – Modelling the World in Data.
Yourdon Press, Prentice Hall.
S. Shlaer & S.J. Mellor (1991):
Object Lifecycles – Modelling the World in States.
Yourdon Press, Prentice Hall.
The Coq Development Team (2010):
The Coq Proof Assistant, Reference Manual.
Available at http://coq.inria.fr/refman.
Xavier Thirioux, Benoît Combemale, Xavier Crégut & Pierre-Loïc Garoche (2007):
A Framework to Formalise the MDE Foundations.
In: TOWERS,
pp. 14–30.
S. Thompson (1999):
Type Theory & Functional Programming.
Computing Laboratory, University of Kent.
eptcs@eptcs.org