Heterogeneous Theory

====================

proof theoretic comorphisms (e.g. CASL->HasCASL, sort gen axs are

only proof theoretically translatable)

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

======================

AMAST 96, Fiadeiro: about parallel composition

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...)

COL / observational logic

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

specify in COL, then project to CASL (= close desgin),

add new sorts, return to COL

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)

Text formatting

===============

Datatype with abstract formatting syntax

different "style sheets" for different output formats (ASCII, HTML, LaTeX)

Priorities of line breaks?

How to handle text width in LaTeX?