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)