ideas revision 67d5e49547d78aa56a8f9ba5e64a950b730eba66
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHeterogeneous Theory
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski====================
83a9571a3df107123eb25f59ac52c576468f2952Till Mossakowskiproof theoretic comorphisms (e.g. CASL->HasCASL, sort gen axs are
83a9571a3df107123eb25f59ac52c576468f2952Till Mossakowski only proof theoretically translatable)
f69658e57cba7ecb37c0d84181f4c563215c2534Till Mossakowskiin favour of comorphisms: subinstitution Eq= -> FOL= is not a morphism
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiTCS-paper: based on WADT 2002 paper, all 8 forms of (co)-morphisms
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (extend HetCASL summary with that)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiShow that any morphism whose image is logically characterizable is
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskialready weakly inducible
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiThe mixed Grothendieck institution is isomorphic to the
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskicomorphism Grothendieck institution, if every morphism is induced
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiby some comorphism and the corresponding 2-cells are there
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski(leading to a quotient)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiSome result of "full abstractness" here? I.e. given
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskia (2-)diagram of certain shape, everything
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiwhich is different at the signature morphism level in
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskithe Grothendieck institution will be different at the
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskicorridor level for suitably chosen institutions,
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskicomorphisms and 2-cells.
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMixed case: use 2-cells between arbitrary paths, based on
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski"relations". Does my Fossacs-Result generalize to the
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskimixed case in this way?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRelation between Grothendieck construction and (co)limits + het. borrwoing
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Do the same "universal pushouts" appear?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLocalized signatures via logics with symbol functor
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski that is faithful and injective on objects
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHeterogeneous examples
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski======================
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till MossakowskiAMAST 96, Fiadeiro: about parallel composition
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiReals in CASL (via HasCASL)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiReals in CASL (via CoCASL) (Lutz?)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski - refinements between these two
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski - both are refinement of first-order reals
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiBIT-Bsp. in CASL-LTL und HasCASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (with morphism keeping the labeled transistion system)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiBsp. von Franzosen (LeGall...)
83a9571a3df107123eb25f59ac52c576468f2952Till MossakowskiCOL / observational logic
83a9571a3df107123eb25f59ac52c576468f2952Till Mossakowski-------------------------
83a9571a3df107123eb25f59ac52c576468f2952Till Mossakowskispecify in COL, then project to CASL (= close desgin),
83a9571a3df107123eb25f59ac52c576468f2952Till Mossakowskiadd new sorts, return to COL
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiGabbay: 19h inf 700 ad/356-1
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski a phi 551 a/387-3 a phi 551 a/387-2
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski tb 3925-1 a mat 038 e/593-1 a mat 038 e/593-2
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- Fiadeiro/Maibaum: Temporal reasoning over deontic specifiations,
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski JLC 1(3) 1991.
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- J.J. Meyer, R. Wieringa: Book about Deontic logic, 1993
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- Fiadeiro, Maibaum: Sometimes tomorrow is sometime:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Action refinement in a temporal logic of objects, LNAI 827
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiModal: how to express K, S4, S5 etc.? (cf. HasCASL: extensionality etc.)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski => sublogics defined by theories (comma signature category)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiKnowledge representation 89:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiK + comp. of modalities
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiK + agreement of modalities (R down S = {x | forall y R(x,y)=>S(x,y)}
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski both decidable, but not their combination
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiOWL-full, 2nd-order DL = non-well-founded sets
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (see Montanari, van Benthem: K + world reachability = non WF elementhood
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski is the same as K)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiFOL + modal logic: interface via propositions
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiFOL + modal logic: interface via making worlds explicit
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski => same for logics for security! (Karsten/Michael)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski IndexedModal --> FOL : make worlds explicit, indices -> data values
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski IndexedModal --> Modal: forget indices (faithful without model expansion?)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski can be used for re-using modal provers
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiBeware: for IPM-->PM borrowing we need proof theoretic conservativity
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiSoftware engeneering
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski--------------------
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- Maibaum: Interconnecting formalisms: supporting
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski modularity, reuse and incrementality. 3rd FSE, ACM press 1995
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- Mainbaum: A mathematical toolbox for the software architect. 11th IWSSD
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (International Workshop on SW spec + design), IEEE press, 1995
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiReactive systems
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski----------------
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiFranzosen aus Toulouse / Boeing: hardware/OS/software, with B/Z
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHeterogeneous refinements
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski HasCASL -> Haskell
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski temporal logic -> CSP
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski --> possibility to mix specification and implementation
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (only parts are implemented)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCSP: see paper by Kwietkowska about CSP + fairness
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiimperative, functional, non deterministic, temporal and real-time aspects
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiask Gunnar Schr�ter! (viewpoint specifications, WADT 2004)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskitimed automata (Michel) + some modal logic?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski(just to have something very different from CASL)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskineeded: non-artifical example involving differen kinds of arrows
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski + which show that universal logic is too complex
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (only a universal "coding" logic would make sense!)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiConsistency / conservativity
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski============================
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiconservativity is right-cancellable; identities/theory isos are cons.
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiimplement check for positiveness of theories
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskisp then op f:t; phi
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiis conservative if sp |- exists f:i . phi
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiConsistency checker: locally + model expansion for the comorphisms
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCraig interpolation
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski===================
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRazvan can show it for the Grothendieck institution?!
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Mail Razvan, send him papers, invite him!
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCR needed for intermediate lemmas (though not necessarily for completeness)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski -> check Marriage example
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Lemma speculation cannot be automatized and is more than CR (Dieter)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMary Sheeran, Chalmers, G�teborg:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski verfication of Haskell programs that construct hardware circuits
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDillian Girow, Stockholm:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski �-calculus for concurrent aspects of Erlang
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiCASL methodology, 3rd volume, ccc tools (Till, Lutz, Cxl)
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiCoCASL/Concurrent Haskell (George's events)/SPIN/CspCASL (Till, Shi, Lutz)
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski Modal-CASL als Anforderungssprache
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski div. Prozessalgebren (wir stellen den allg. Rahmen)
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiManagement of change (bkb, Hutter, Till, cxl, Achim, Kohlhase?)
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiOntologien: neuer SFB-Antrag (Fr�hjahr 2005)
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiAbstract robotics (cxl, paolo)
f3a84cc409ed345569be6673d05072dcb4291ebeTill MossakowskiAWE II / General FM (cxl, bkb)
f3a84cc409ed345569be6673d05072dcb4291ebeTill MossakowskiText formatting
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski===============
f3a84cc409ed345569be6673d05072dcb4291ebeTill MossakowskiDatatype with abstract formatting syntax
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowskidifferent "style sheets" for different output formats (ASCII, HTML, LaTeX)
f3a84cc409ed345569be6673d05072dcb4291ebeTill MossakowskiPriorities of line breaks?
f3a84cc409ed345569be6673d05072dcb4291ebeTill MossakowskiHow to handle text width in LaTeX?