Heterogeneous Theory
====================

in favour of comorphisms: subinstitution Eq= -> FOL= is not a morphism

TCS-paper: based on WADT 2002 paper, all 8 forms of (co)-morphisms
  (extend HetCASL summary with that)

Show that any morphism whose image is logically characterizable is
already weakly inducible

The mixed Grothendieck institution is isomorphic to the
comorphism Grothendieck institution, if every morphism is induced
by some comorphism and the corresponding 2-cells are there
(leading to a quotient)

Some result of "full abstractness" here? I.e. given
a (2-)diagram of certain shape, everything
which is different at the signature morphism level in
the Grothendieck institution will be different at the
corridor level for suitably chosen institutions,
comorphisms and 2-cells.

Mixed case: use 2-cells between arbitrary paths, based on
"relations". Does my Fossacs-Result generalize to the
mixed case in this way?

Relation between Grothendieck construction and (co)limits + het. borrwoing
  Do the same "universal pushouts" appear?

Localized signatures via logics with symbol functor
  that is faithful and injective on objects

Heterogeneous examples
======================

Reals in CASL (via HasCASL)
Reals in CASL (via CoCASL) (Lutz?)
  - refinements between these two
  - both are refinement of first-order reals
BIT-Bsp. in CASL-LTL und HasCASL
  (with morphism keeping the labeled transistion system)
ETAPS-Typ
Saarbrücker Bsp.e
Bsp. von Franzosen (LeGall...)

Modal logics
------------
Gabbay: 19h inf 700 ad/356-1
      a phi 551 a/387-3   a phi 551 a/387-2
     tb 3925-1    a mat 038 e/593-1     a mat 038 e/593-2
- Fiadeiro/Maibaum: Temporal reasoning over deontic specifiations, 
  JLC 1(3) 1991.
- J.J. Meyer, R. Wieringa: Book about Deontic logic, 1993
- Fiadeiro, Maibaum: Sometimes tomorrow is sometime: 
  Action refinement in a temporal logic of objects, LNAI 827

Modal: how to express K, S4, S5 etc.? (cf. HasCASL: extensionality etc.)
      => sublogics defined by theories (comma signature category)
Knowledge representation 89:
K + comp. of modalities
K + agreement of modalities (R down S = {x | forall y R(x,y)=>S(x,y)}
  both decidable, but not their combination
OWL-full, 2nd-order DL = non-well-founded sets
   (see Montanari, van Benthem: K + world reachability = non WF elementhood
                                is the same as K)

FOL + modal logic: interface via propositions
FOL + modal logic: interface via making worlds explicit
    => same for logics for security! (Karsten/Michael)
    IndexedModal --> FOL : make worlds explicit, indices -> data values
    IndexedModal --> Modal: forget indices (faithful without model expansion?)
                            can be used for re-using modal provers
Beware: for IPM-->PM borrowing we need proof theoretic conservativity

Software engeneering 
--------------------
- Maibaum: Interconnecting formalisms: supporting
  modularity, reuse and incrementality. 3rd FSE, ACM press 1995
- Mainbaum: A mathematical toolbox for the software architect. 11th IWSSD
  (International Workshop on SW spec + design), IEEE press, 1995


Reactive systems
----------------
Franzosen aus Toulouse / Boeing: hardware/OS/software, with B/Z
Heterogeneous refinements
  HasCASL -> Haskell
  temporal logic -> CSP
  --> possibility to mix specification and implementation
      (only parts are implemented)

CSP: see paper by Kwietkowska about CSP + fairness

Grosse-Rhode
imperative, functional, non deterministic, temporal and real-time aspects
ask Gunnar Schröter! (viewpoint specifications, WADT 2004)

timed automata (Michel) + some modal logic?
(just to have something very different from CASL)

needed: non-artifical example involving differen kinds of arrows
        + which show that universal logic is too complex
          (only a universal "coding" logic would make sense!)


Consistency / conservativity
============================
conservativity is right-cancellable; identities/theory isos are cons.
implement check for positiveness of theories
sp then op f:t; phi
is conservative if sp |- exists f:i . phi

Consistency checker: locally + model expansion for the comorphisms


Craig interpolation
===================
Razvan can show it for the Grothendieck institution?!
  Mail Razvan, send him papers, invite him!
CR needed for intermediate lemmas (though not necessarily for completeness)
  -> check Marriage example
  Lemma speculation cannot be automatized and is more than CR (Dieter)


Haskell
=======
Mary Sheeran, Chalmers, Göteborg: 
  verfication of Haskell programs that construct hardware circuits
Dillian Girow, Stockholm:
  µ-calculus for concurrent aspects of Erlang

DOLCE
=====
Ontoclean


DFG projects
============
CASL methodology, 3rd volume, ccc tools (Till, Lutz, Cxl)
CoCASL/Concurrent Haskell (George's events)/SPIN/CspCASL (Till, Shi, Lutz)
   Modal-CASL als Anforderungssprache
   div. Prozessalgebren (wir stellen den allg. Rahmen)
Management of change (bkb, Hutter, Till, cxl, Achim, Kohlhase?)
HetCASL/Hets (Till)
Ontologien: neuer SFB-Antrag (Frühjahr 2005)
Abstract robotics (cxl, paolo)
AWE II / General FM (cxl, bkb)