REMICS was participating at 2nd International Conference on Model & Data Engineering (MEDI’2012) (http://medi2012.ensma.fr/program.html)
F.Barbier, E.Cariou : Inductive UML, proceedings of 2nd International Conference on Model & Data Engineering, Poitiers, France, Lecture Notes in Computer Science #7602, Springer, October 3-5, 2012
The increasing importance of metamodeling calls for metamodels that are free of ambiguities, contradictions and redundancies. This is specifically the case for the core of UML (Infrastructure). This paper proposes to rewrite a part of this core, the Class and Property metaclasses especially. To avoid infinite regression, the notion of meta-circularity is used. This rewriting is done by means of inductive types in constructive logic. The proposed specification is proven correct using the Coq automated prover. Proven lemmas and theorems about a “metaness” relationship are proposed.