Woodcut by Jiri Daschitzsky, Von einem Schrecklichen und Wunderbahrlichen Cometen so sich den Dienstag nach Martini M. D. Lxxvij. Jahrs am Himmel erzeiget hat (Prague (?): Petrus Codicillus a Tulechova, 1577)

CoMeta - Computational Metamodels

Home Meetings Documents and Reports Publications
Tasks Mailing list Related Projects Tools

NEWS

The final workshop of the project is approaching!

Description

The CoMeta project is partially funded by the Ministero dell'Istruzione, Università e Ricerca (MIUR). The project number is COFIN 2001013518. The duration is 24 months (2002-2003).

Scientific Coordinator: Furio Honsell

Principal Partners and Contacts:

Summary of Project

Computer Science has grown into a complex discipline, with scientific and technological sides to it, which intersects various knowledge domains at once, and acts at various levels of abstraction. In order to put into focus the present project, it appears convenient to distinguish two metalevels, above the basic one, which is the one where hardware and software systems live.
The semantical and syntactical tools which are normally used to specify and analyze the object level systems appear on the first of these metalevels. This is the abstraction level of programming and specification languages, of calculi, of denotational and operational models, of automata, of Petri Nets, etc., but it is also the level of the logical systems used in verfying and analyzing properties of programs and processes, etc.
The development of Computer Science in the last decades has indicated clearly 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 Milner's action structures, Logical Frameworks, Rewriting Logics, Graph Grammars.
The present project originates 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 intend to study general issues concerning computational metamodels, and to explore 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 shall focus 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.
We will explore the usability of each of these metamodels and we shall compare the advantages of the different representations that each of these provide, for various systems arising in the areas of concurrency and mobility, which are so important in the present era of global computing. These case studies should justify the existence of so many different metamodels. We will develop methodologies for transfering techniques and constructions between different encodings within one metamodel, and between different metamodels. Finally we will define a benchmark for metamodels.
The project is structured along four different tracks, corrsponding to four different perspectives on metamodels:
  1. Logical Frameworks. Leader: F.Honsell, Udine.
  2. Transition and Rewriting systems. Leader : U.Montanari, Pisa
  3. Logical Semantics. Leader: S.Ronchi della Rocca, Torino.
  4. Categories with Structure. Leader: N. Sabadini, Como.
Site maintainer: Marino Miculan Last modified: Tue Aug 27 09:51:15 CEST 2002