DISI Dipartimento di Informatica e Scienze dell'Informazione


Relationships between Logical Frameworks

E. Astesiano and M. Cerioli .

In Recent Trends in Data Type Specification, number 655 in Lecture Notes in Computer Science, pages 126--143, Berlin, 1993. Springer Verlag.

Adopting the concept of institution to represent logical frames, we have introduced in a previous paper the concept of simulation of an institution by another.
Here we first show how simulations can be used to investigate the relationships between frames, distinguishing three levels, corresponding to different kinds of simulations: ``set-theoretic'', where the individual models of different frames are related disregarding their categorical and logical interconnection, ``categorical'', where the relation is between the categories of models, and ``logical'', where the relation is between specifications.
Then we propose a concept of translation of inference systems along simulations such that soundness and completeness are preserved.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/CerioliM/WADT92.ps.z (73265 Kb)