Publikation
A Proof Theoretic Interpretation of Model Theoretic Hiding
Mihai Codescu; Fulya Horozal; Michael Kohlhase; Till Mossakowski; Florian Rabe
In: Hans-Jörg Kreowski; Till Mossakowski (Hrsg.). Recent Trends in Algebraic Development Techniques. International Workshop on Algebraic Development Techniques (WADT-10), 20th, July 1-4, Schloss Etelsen, Germany, Pages 118-138, Lecture Notes in Computer Science (LNCS), Vol. 7137, Springer, 2012.
Zusammenfassung
Logical frameworks like LF are used for formal representa-
tions of logics in order to make them amenable to formal machine-assisted
meta-reasoning. While the focus has originally been on logics with a proof
theoretic semantics, we have recently shown how to define model
theoretic logics in LF as well. We have used this to define new institutions in
the Heterogeneous Tool Set in a purely declarative way.
It is desirable to extend this model theoretic representation of logics to
the level of structured specifications. Here a particular challenge among
structured specification building operations is hiding, which restricts a
specification to some export interface. Specification languages like ASL
and CASL support hiding, using an institution-independent model
theoretic semantics abstracting from the details of the underlying logical
system.
Logical frameworks like LF have also been equipped with structuring
languages. However, their proof theoretic nature leads them to a theory-
level semantics without support for hiding. In the present work, we show
how to resolve this difficulty.