todo revision f1ba3c4b1394e88800bece2e9067e2866015cfeb
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPlan and priority list for CoFI tool activities
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiSonja (Till)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHaskell parser f�r XHaskell erweitern
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDimplom: Encoding for HasCASL in Isabelle/HOL(CF)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiJorina (Till)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskidevelopment graph calculus
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowski- Stack overflow for "show just subtree"
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowski- view-test7.casl should be provable with globDecomp + locDecopm
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowski- fail when doing first globDecomp, then local decomp in RelationsAndOrders
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMartin (Till)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskitype check for CASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiif a subterm is not typeable at all, output it
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
38f30f746aa42d4fc659a15e183801f2f74596d0Till MossakowskiMingyi (Till)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski cd /home/cofi/xinga/src/uni
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski gmake packages
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski cd /home/cofi/xinga/src/HetCATS
38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski make hets
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski
38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowskitry out small examples, e.g.
38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski export HETS_LIB=.../CASL-lib
38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski hets .../CASL-lib/Basic/Algebra_I.casl
38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowskilook at HetCATS/README
38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski
ed892c579cca270fff0aa9cc2a34351c420e3182Till MossakowskiTest auf Einpunkt-Modell
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski (ein Datenelement, wahre Pr�dikate, totale Funktionen)
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski siehe ccc/OnePoint.hs
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski
88c65bd4e8841502546923da0e81ade9045e8fecTill MossakowskiSignature morphism: just carry around the image
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskiuse three-valued logic {true, false, *}, * means "don't know"
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskiequations between new sorts are true, otherwise *
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskinew predicates are true, otherwise *
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskiand t f *
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskit t f *
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskif f f f
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski* * f *
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskior t f *
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskit t t t
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskif t f *
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski* t * *
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskiimplies t f *
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskit t f *
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskif t t t
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski* t * *
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskiequivalent t f *
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskit t f *
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskif f t *
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski* * * *
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowskinot t f *
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski f t *
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski(this is just Kleene's strong three-valued logic)
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski
88c65bd4e8841502546923da0e81ade9045e8fecTill MossakowskiImplement it using Maybe Bool and monads
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski
88c65bd4e8841502546923da0e81ade9045e8fecTill MossakowskiSort generation constraints:
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski use recover_sort_gen
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski check whether all generated sorts (when translated via the sort map) are new
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski check whether for each generated sort,
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski there is a term with generating operations
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski and variables in non-generated sorts
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski Therefore start with the empty list of sorts, and repeatedly
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski compute the one-step-closure under the generating operations
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski (ignoring argument sorts outside the generated sorts)
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski stop when iteration is stable
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowskiport CCC to Haskell
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiZicheng (Till)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowskicvs -d :pserver:mnd@.... login
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowskicvs -d :pserver:mnd@.... checkout HetCATS
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiTranslation from CASL with subsorts to CASL without subsorts
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowskicvs -d :pserver:cvsread@.... login
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowskicvs -d :pserver:cvsread@.... checkout CATS
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowskisee CATS/basic_encode.sml, encode SubCFOL into CFOL
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowskiencode subsorting by injection functions
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski1. translation of signatures (see HetCATS/CASL/Sign.hs)
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski2. genertion of axioms (injectivity, overloading ...)
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski (see HetCATS/CASL/AS_Basic_CASL.hs)
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowskidetails: see paper in Theoretical Computer Science, p. 407
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiAngucken:
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski FORMULA in CASL/AS_Basic.hs
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski Sign in CASL/Sign.hs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHeng (Klaus)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLaTeX pretty printer
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiChristian
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
dedca4980b2d43bc343ffcaf73e0617524f9720cTill MossakowskiMissing points for heterogeneous WADT 04 example:
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski- translation of sentences along HasCASL sig mors
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski- correct display of HasCASL sublogis
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski- improve display of HasCASL sigs + mors
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski- translation of sentences CASL->HasCASL
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiSprachdesign HasCASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Verh�ltnis von Parametrisierung und Polymorphie/Typklassen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiStatic analysis for HasCASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Subsorting
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Symbol map analysis
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiWeak amalgamation analysis
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiInstantiate Transformation Application system for HasCASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAutomatic generation of Haskell (for a HasCASL subset)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiProofs in HasCASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCase study
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiS�nke Magnussen kontaktieren (der arbeitet mit Has-CASL-�hnlicher Sprache)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiKlaus
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskivisualization of "taxonomy" of CASL signatures
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (subsorts = inheritance, unary preds = concepts, binary preds = relations)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRecognize guarded fragment of CASL:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski G ::= forall x . At(x) => G where At is a conjunction of atoms
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski | exists x . At(x) /\ G
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiJoost Visser wg. ATerms in Haskell => neues Repository
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMarkus, Lutz
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiBeweise in Isabelle
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCASL consistency checker
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (Vorbild: Larch-Handbuch)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiParser and static analysis for CSP-CASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiChristoph
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCASL consistency checker
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIsaWin: support CASL-libraries
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMaciek
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiStatic analysis of architectural specs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiTill
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowski- List[Dec] wird List[Pos]
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski- George wg. Schlie�en von Fenstern
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowski- node numbers do not match
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski- thm links with external target should be provable as well
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowski
dedca4980b2d43bc343ffcaf73e0617524f9720cTill MossakowskiMissing points for heterogeneous WADT 04 example:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- coding to Isabelle: translate sort gen constraints
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski- remove / in thy names (ask cxl for function)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- problem with Ids starting with __ (look at Isabelle's lexis)
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski- correct display of CASL sublogis
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- correct MAYA: glob decomp: some links are not found (Jorina)
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski- extended globDecomp rule: existing local Thm links
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski (e.g. generated by %implied) should lead to fewer new local
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski links ("local composition" rule)
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiModal logics: modal logic, temporal logic, mu calculus
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski+ translations (e.g. modal to FOL)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIsabelle: (ask Christoph)
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski correct show theory
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski Keep proofs and lemmas in .thy files (kind of merge)
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski prove local thm link (=> green)
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski better interaction between Isabelle instance (for one node)
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski + selection of single goals that are proved
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski => use PGIP interface (Christoph, David)
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski CASL-like syntax
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski CASL annotation for lemmas that should be used in proof
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski inherit CASL's mixfix syntax
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRemove warnings
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDifferent types of logic translations
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiImprove Static analysis of structured specs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDevelopment graph calculus, Strategies for DG rules
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiManagement of change
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIntegrate provers
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Otter model checker
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
f69658e57cba7ecb37c0d84181f4c563215c2534Till Mossakowski Isabelle codings: www.inf.ethz.ch/~vigano
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Renate Schmidt, Manchester: uses FOL prover for description logic
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (as efficient as DL-specific tools!)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Look at PROSPER toolkit
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski consistency: see IJCAR-workshop on non-provability in Cork
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski IJCAR workshop about logical frameworks and meta-languages
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIntegrate CCC
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEncodings
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiErrors:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiTest suite (Christian's mail)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiKlaus' wayfinding example
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUniForM workbench:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifirst steps towards CASL instance, using ATerms and re-using MMISS instance
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskivariants for specs (needed for DOLCE: CASL variant, DL variant, ...)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIntegration of MAYA and Isabelle/HOL (global HOL-Coding of
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Grothendieck logic)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski + for TAS: reflection of HOL in HOL, to be composed with encodings
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (i.e. signatures, axioms, signature morphisms in HOL,
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski re-use ML signatures) (Einar)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDisplay Specs as daVinci subgraphs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUser interface
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski--------------
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLogic graph window
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiInput text window
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDevelopment graph window
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiProver windows
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiFOR STUDENTS
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEmacs mode
38f30f746aa42d4fc659a15e183801f2f74596d0Till MossakowskiHets Web interface (cf. CATS/web_interface2.sml)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCCC ?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPackaging of installation
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiintegrate QuickCheck
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiXML interface
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiGUI (vgl. VSE)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiincrease performance
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski++++++++++++++++++++++++++++++++++++++++++++++++
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRemaining things
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski++++++++++++++++++++++++++++++++++++++++++++++++
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Coq, PTT in Maude
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiProof general interface (1 day)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiTest Maya with basic datatypes
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiVerbesserung der Fehlermeldungen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiImprove encoding: CATS/basic_encode.sml (3 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMore HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRenamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiExample of Agnes und Frank: proofs in HOL-CASL (2 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiTerm input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiExamples for cond rewriting -> Christophe
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDoku: VSE-Prover, VSE-Method VSE-demo in Bremen?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAdapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEigene IsaWin-Instanz mit CASL-RS statt HOL-RS
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEncoding of structured free (3 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEncoding of structured cofree (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEingabesyntax als Mix zwischen CASL und HOL (3 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAdapt Isabelle unions to CASL unions (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIsaWin git/src/isa_ext/casl_thy.sml (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiGenerate Proof obligations (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAdd renaming to Isabelle kernel (2 months)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiBasic datatypes CASL-lib/Basic/basic.casl
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRepository mit korrekten und fehlerhaften Specs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHetCATS User manual, Doku fuer Environments (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiConversion ASF/SDF-Parser -> abstract syntax (in Haskell)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiComparsion of parsers (ML-yacc parser, SDF-Parser)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiConversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPVS anbinden (Kooperation mit Cachan?)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPortations: Intel-Solaris, Mac OS-10 (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiViews on CASL specs: CATS/viewer.sml (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiModule graph CATS/module_graph.sml (1 week) -> Maya?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiATerms via XML: CATS/aterms.sml (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiNeues Tool-Schaubild auf Web-Seiten ver�ffentlichen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLibrary management: CATS/lib_ana.sml (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiVersion management/Uniform Workbench: CATS/lib_ana.sml (2 months)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski{- This does not work due to needed ordering:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiinstance Functor Set where
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski fmap = mapSet
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiinstance Monad Set where
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski return = unitSet
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski m >>= k = unionManySets (setToList (fmap k m))
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski-}