0N/Ain favour of comorphisms: subinstitution Eq= -> FOL= is not a morphism
0N/ATCS-paper: based on WADT 2002 paper, all 8 forms of (co)-morphisms
0N/A (extend HetCASL summary with that)
0N/AShow that any morphism whose image is logically characterizable is
0N/Aalready weakly inducible
0N/AThe mixed Grothendieck institution is isomorphic to the
0N/Acomorphism Grothendieck institution, if every morphism is induced
0N/Aby some comorphism and the corresponding 2-cells are there
0N/A(leading to a quotient)
0N/ASome result of "full abstractness" here?
I.e. given
2362N/Aa (2-)diagram of certain shape, everything
2362N/Awhich is different at the signature morphism level in
2362N/Athe Grothendieck institution will be different at the
0N/Acorridor level for suitably chosen institutions,
0N/Acomorphisms and 2-cells.
0N/AMixed case: use 2-cells between arbitrary paths, based on
0N/A"relations". Does my Fossacs-Result generalize to the
0N/Amixed case in this way?
0N/ARelation between Grothendieck construction and (co)limits + het. borrwoing
0N/A Do the same "universal pushouts" appear?
0N/ALocalized signatures via logics with symbol functor
0N/A that is faithful and injective on objects
0N/AHeterogeneous examples
0N/A======================
0N/AReals in CASL (via HasCASL)
0N/AReals in CASL (via CoCASL) (Lutz?)
0N/A - refinements between these two
0N/A - both are refinement of first-order reals
0N/ABIT-Bsp. in CASL-LTL und HasCASL
0N/A (with morphism keeping the labeled transistion system)
0N/ABsp. von Franzosen (LeGall...)
0N/AGabbay: 19h inf 700 ad/356-1
0N/A a phi 551 a/387-3 a phi 551 a/387-2
0N/A tb 3925-1 a mat 038 e/593-1 a mat 038 e/593-2
0N/A-
J.J. Meyer, R. Wieringa: Book about Deontic logic, 1993
0N/A- Fiadeiro, Maibaum: Sometimes tomorrow is sometime:
0N/A Action refinement in a temporal logic of objects, LNAI 827
0N/AModal: how to express K, S4, S5 etc.? (cf. HasCASL: extensionality etc.)
0N/A => sublogics defined by theories (comma signature category)
0N/AKnowledge representation 89:
0N/AK + comp. of modalities
0N/AK + agreement of modalities (R down S = {x | forall y R(x,y)=>S(x,y)}
0N/A both decidable, but not their combination
0N/AOWL-full, 2nd-order DL = non-well-founded sets
0N/A (see Montanari, van Benthem: K + world reachability = non WF elementhood
0N/AFOL + modal logic: interface via propositions
0N/AFOL + modal logic: interface via making worlds explicit
0N/A IndexedModal --> FOL : make worlds explicit, indices -> data values
0N/A IndexedModal --> Modal: forget indices (faithful without model expansion?)
0N/A can be used for re-using modal provers
0N/ABeware: for IPM-->PM borrowing we need proof theoretic conservativity
0N/A- Maibaum: Interconnecting formalisms: supporting
0N/A modularity, reuse and incrementality. 3rd FSE, ACM press 1995
0N/A- Mainbaum: A mathematical toolbox for the software architect. 11th IWSSD
0N/A (International Workshop on SW spec + design), IEEE press, 1995
0N/AHeterogeneous refinements
0N/A temporal logic -> CSP
0N/A --> possibility to mix specification and implementation
0N/A (only parts are implemented)
0N/ACSP: see paper by Kwietkowska about CSP + fairness
0N/Aimperative, functional, non deterministic, temporal and real-time aspects
0N/Aask Gunnar Schr�ter! (viewpoint specifications, WADT 2004)
0N/Atimed automata (Michel) + some modal logic?
0N/A(just to have something very different from CASL)
0N/Aneeded: non-artifical example involving differen kinds of arrows
0N/A + which show that universal logic is too complex
0N/A (only a universal "coding" logic would make sense!)
0N/AConsistency / conservativity
0N/A============================
0N/Aimplement check for positiveness of theories
0N/Ais conservative if sp |- exists f:i . phi
0N/AConsistency checker: locally + model expansion for the comorphisms
0N/ARazvan can show it for the Grothendieck institution?!
0N/A Mail Razvan, send him papers, invite him!
0N/ACR needed for intermediate lemmas (though not necessarily for completeness)
0N/A -> check Marriage example
0N/A Lemma speculation cannot be automatized and is more than CR (Dieter)
0N/AMary Sheeran, Chalmers, G�teborg:
0N/A verfication of Haskell programs that construct hardware circuits
0N/ADillian Girow, Stockholm:
0N/A �-calculus for concurrent aspects of Erlang
0N/ACASL methodology, 3rd volume, ccc tools (Till, Lutz, Cxl)
0N/A Modal-CASL als Anforderungssprache
0N/A div. Prozessalgebren (wir stellen den allg. Rahmen)
0N/AManagement of change (bkb, Hutter, Till, cxl, Achim, Kohlhase?)
0N/AOntologien: neuer SFB-Antrag (Fr�hjahr 2005)
0N/AAbstract robotics (cxl, paolo)
0N/AAWE II / General FM (cxl, bkb)