@Article{jung99,
author = {A. Jung and M. Kegelmann and M. A. Moshier},
title = {Multi lingual sequent calculus and coherent spaces},
journal = {Fundamenta Informaticae},
year = {1999},
volume = {37},
pages = {369--412}
abstract = {We study a Gentzen style sequent calculus where the
formulas on the left and right of the turnstile need
not necessarily come from the same logical system.
Such a sequent can be seen as a consequence between
different domains of reasoning. We discuss the
ingredients needed to set up the logic generalized
in this fashion.
The usual cut rule does not make sense for sequents
which connect different logical systems because it
mixes formulas from antecedent and succedent. We
propose a different cut rule which addresses this
problem.
The new cut rule can be used as a basis for
composition in a suitable category of logical
systems. As it turns out, this category is
equivalent to coherent spaces with certain relations
between them.
Finally, cut elimination in this set-up can be
employed to provide a new explanation of the domain
constructions in Samson Abramsky's Domain
Theory in Logical Form.}
}