[en] Formal modeling systems such as the Unified Modeling Language (UML), are widely used by software engineers. Such systems allow reasoning about the large-scale organization of information systems, easing their analysis, design and implementation, reducing maintenance costs and simplifying automated generation or refactoring of software. On the other hand, despite the success that these tools have experienced, they are not devoid of limi-tations. Perhaps the most noticeable is the lack of support for more than one level of instantiation of a certain class. In order to solve this problem, extensions have been designed, such as the Meta-Object Facility (MOF), that expand the functionality of classical modeling frameworks allowing additional levels between which can be established instance-of relationships. Multilevel metamodelling or deep metamodelling is a recently-developed modeling paradigm that aims to completely eliminate the restrictions inherent in the four-layer approach proposed by the MOF, re-placing them with systems that allow for an unrestricted number of object layers. However, the current un-derstanding of this tool is based on category theory, a mathematical abstraction that is hard to relate to real object-oriented programming. In order to better understand the particularities of this new tool, putting it in context with the existing theory and facilitating subsequent research, this work intends to establish a formalization of said tool through the use of type theory, a branch of computer science that deals with the specification and semantics of typing rules for programming languages and similar formal systems. With this in mind, we've developed and analyzed two formal systems that intend to form the basis for the development of further programming languages based on the notions of multilevel metamodelling. Furthermore, we have developed compilers for said systems that show the practical applicability of these purely theoretical models.

[es] Los sistemas formales de modelado, como el Unified Modeling Language (UML), son bien cono-cidos por todos los ingenieros de software. Los mismos permiten razonar sobre la estructura a gran escala de los sistemas de la información, facilitando el análisis, diseño e implementación de los mismos, así como su mantenimiento posterior, y simplificando tareas como la refactorización automática o la generación de códi-go. Por otro lado, a pesar del éxito que han tenido estas herramientas, no están exentas de limitaciones. La más notable de las mismas es, quizás, que no se permite considerar más de un nivel de instanciación de una clase. Para solventar esta insuficiencia, existen extensiones, como el Meta-Object Facility (MOF), que aumentan esta funcionalidad añadiendo niveles adicionales entre los que se pueden establecer relaciones de instanciación. El metamodelado multinivel o metamodelado profundo es un paradigma relativamente nuevo de modelado que elimina las restricciones de la estructura estándar de cuatro capas que propone el MOF permi-tiendo sistemas con un número arbitrario de niveles. Sin embargo, el entendimiento actual de esta herra-mienta está basado en nociones de teoría de categorías, una disciplina matemática que resulta difícil de to-mar en relación a lenguajes de programación reales orientados a objetos. Para comprender mejor el funcionamiento de esta nueva herramienta, poniéndola en contexto con la teoría existente, y dar pie a investigación futura, este trabajo pretende establecer una formalización de la misma basada en teoría de tipos, una rama de la teoría de la computación que estudia la semántica de las reglas de tipado en un lenguaje de programación o sistema similar. Con este objetivo, hemos construido y analizado dos sistemas formales que pretenden constituir la base del desarrollo de futuros lenguajes de pro-gramación basados en el metamodelado multinivel, y hemos desarrollado compiladores de los mismos a Ja-vaScript para probar la aplicabilidad de estos modelos teóricos de manera práctica.