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

------------

- 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