COMETA
MIUR COFIN 2001013518 (01/2002-12/2003)
Project COMETA was about Computational Metamodels. The starting observation was that there is no chance to come up some day with the universal programming or modeling language, or with the ultimate universal computational logic. We have to live with a plethora of different calculi and special-purpose formalisms, and we have to be constantly ready to develop new conceptual frameworks. But we do not want to start over from first principles the theory of each and every one of these systems, calculi or logics. Nor we want to reimplement from scratch, for each of them, suitable interactive tools for manipulating them rigorously. It is inevitable therefore to conceive another abstraction level above the first one, where commonalities across different systems can be focused and factored out. On this level we can define framework theories within which to prove structural results which prevent us from duplicating efforts in developing the metathoery of the lower level systems. This second metalevel is the level of “computational metamodels”. Examples of these are action structures, bigraphs, Logical Frameworks, Rewriting Logics, Graph Grammars.
The COMETA project originated from the consideration that reductionism is not even conceivable, however, at the level of metamodels. A universal metamodel is just as utopian as a universal progrmming language. If we want to keep the mathematical overhead in representations to a minimum and have simple and transparent encodings we have to entertain more than one computational metamodel. In this project we studied general issues concerning computational metamodels, and explored the possibility of utilizing successfully as computational metamodels some logical and categorical frameworks recently proposed, also by some of the researchers involved in this project. In particular we focused on Logical Frameworks based on constructive type theories and exploiting higher order abstract syntax, on various syntax-free approaches to concurrency and mobility (such as Tile Logics, double categories, graph transformation systems, bialgebras, and the categorical algebra of cospan-span of graphs), and on systems of logical semantics based on implicit intersection type theories.
In that project I deepened my interests in concurrent and distributed systems, and returned to category theory.