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