todo revision e539b8cb4a47f987bc57c90ee964219ac53841ff
750f77ade4110c6b2315d6b9e9c22f643914d87drbbPlan and priority list for CoFI tool activities
7a6c08288f79ab1734b98afc114e52cd71f898c0jwoolley
750f77ade4110c6b2315d6b9e9c22f643914d87drbb
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe************************************************
750f77ade4110c6b2315d6b9e9c22f643914d87drbbSonja (Till)
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe************************************************
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme
750f77ade4110c6b2315d6b9e9c22f643914d87drbbHaskell parser f�r XHaskell erweitern
750f77ade4110c6b2315d6b9e9c22f643914d87drbbDimplom: Encoding for HasCASL in Isabelle/HOL(CF)
750f77ade4110c6b2315d6b9e9c22f643914d87drbb
750f77ade4110c6b2315d6b9e9c22f643914d87drbb************************************************
750f77ade4110c6b2315d6b9e9c22f643914d87drbbJorina (Till)
750f77ade4110c6b2315d6b9e9c22f643914d87drbb************************************************
7a6c08288f79ab1734b98afc114e52cd71f898c0jwoolley
7a6c08288f79ab1734b98afc114e52cd71f898c0jwoolleydevelopment graph calculus
45108af9f7bc456c8e9b3bf3ea863f171e6dc9a6jwoolley
7a6c08288f79ab1734b98afc114e52cd71f898c0jwoolley************************************************
3e5667f3bea0b417d0133534d960c5b86c63cf5cgsteinMartin (Till)
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme************************************************
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemmetype check for CASL
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemmeif a subterm is not typeable at all, output it
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme************************************************
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemmeMingyi (Till)
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme************************************************
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme cd /home/cofi/xinga/src/uni
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme gmake packages
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme cd /home/cofi/xinga/src/HetCATS
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme make hets
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemmetry out small examples, e.g.
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme export HETS_LIB=.../CASL-lib
3e5667f3bea0b417d0133534d960c5b86c63cf5cgstein hets .../CASL-lib/Basic/Algebra_I.casl
7a6c08288f79ab1734b98afc114e52cd71f898c0jwoolleylook at HetCATS/README
7a6c08288f79ab1734b98afc114e52cd71f898c0jwoolley
7a6c08288f79ab1734b98afc114e52cd71f898c0jwoolleyTest auf Einpunkt-Modell
7a6c08288f79ab1734b98afc114e52cd71f898c0jwoolley (ein Datenelement, wahre Pr�dikate, totale Funktionen)
7a6c08288f79ab1734b98afc114e52cd71f898c0jwoolley siehe ccc/OnePoint.hs
750f77ade4110c6b2315d6b9e9c22f643914d87drbb
105475009f541187ba7a14a367547d9404c578befieldingport CCC to Haskell
7a6c08288f79ab1734b98afc114e52cd71f898c0jwoolley
7a6c08288f79ab1734b98afc114e52cd71f898c0jwoolley************************************************
7a6c08288f79ab1734b98afc114e52cd71f898c0jwoolleyZicheng (Till)
750f77ade4110c6b2315d6b9e9c22f643914d87drbb************************************************
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme
7a6c08288f79ab1734b98afc114e52cd71f898c0jwoolley
750f77ade4110c6b2315d6b9e9c22f643914d87drbb************************************************
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewroweHeng (Klaus)
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe************************************************
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewroweLaTeX pretty printer
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme************************************************
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewroweChristian
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe************************************************
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemmeSprachdesign HasCASL
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme Verh�ltnis von Parametrisierung und Polymorphie/Typklassen
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemmeStatic analysis for HasCASL
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe Subsorting
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemme Symbol map analysis
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewroweWeak amalgamation analysis
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewroweInstantiate Transformation Application system for HasCASL
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewroweAutomatic generation of Haskell (for a HasCASL subset)
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewroweProofs in HasCASL
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewroweCase study
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewroweS�nke Magnussen kontaktieren (der arbeitet mit Has-CASL-�hnlicher Sprache)
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe************************************************
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewroweKlaus
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe************************************************
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowevisualization of "taxonomy" of CASL signatures
6f4e1cd73ca28a9876f1a37a6cdfd613eab6ec37wrowe (subsorts = inheritance, unary preds = concepts, binary preds = relations)
6f4e1cd73ca28a9876f1a37a6cdfd613eab6ec37wroweRecognize guarded fragment of CASL:
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe G ::= forall x . At(x) => G where At is a conjunction of atoms
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe | exists x . At(x) /\ G
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewroweJoost Visser wg. ATerms in Haskell => neues Repository
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe************************************************
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewroweMarkus, Lutz
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe************************************************
c6db3f5916ebd715971c3db837be9143394f8aa9slive
c6db3f5916ebd715971c3db837be9143394f8aa9sliveBeweise in Isabelle
c6db3f5916ebd715971c3db837be9143394f8aa9sliveCASL consistency checker
c6db3f5916ebd715971c3db837be9143394f8aa9sliveWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
ce4eec7f83c4bc6daba6a02eff0275a6f3878e5ewrowe (Vorbild: Larch-Handbuch)
39c36cbd2a461e4fe1bdd0a860db587d420445c7sctemmeSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
750f77ade4110c6b2315d6b9e9c22f643914d87drbbParser and static analysis for CSP-CASL
7a6c08288f79ab1734b98afc114e52cd71f898c0jwoolley
7a6c08288f79ab1734b98afc114e52cd71f898c0jwoolley************************************************
Christoph
************************************************
CASL consistency checker
IsaWin: support CASL-libraries
************************************************
Maciek
************************************************
Static analysis of architectural specs
************************************************
Till
************************************************
try out WADT 04 example:
- coding to Isabelle: translate sort gen constraints
- translation of sentences CASL->HasCASL (Christian)
- translation of sentences along HasCASL sig mors (Christian)
- remove / in thy names
- problem with Ids starting with __ (look at Isabelle's lexis)
- correct display of CASL sublogis
- improve display of HasCASL sigs + mors (Christian)
- correct display of HasCASL sublogis (Christian)
- correct MAYA: glob decomp: some links are not found (Jorina)
Modal logics: modal logic, temporal logic, mu calculus
+ translations (e.g. modal to FOL)
Isabelle: (ask Christoph)
correct show theory
Keep proofs and lemmas in .thy files (kind of merge)
prove local thm link (=> green)
better interaction between Isabelle instance (for one node)
+ selection of single goals that are proved
CASL-like syntax
CASL annotation for lemmas that should be used in proof
Remove warnings
Different types of logic translations
Improve Static analysis of structured specs
Development graph calculus, Strategies for DG rules
Management of change
Integrate provers
Otter model checker
modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
Isabelle codings: www.inf.ethz.ch/~vigano
Renate Schmidt, Manchester: uses FOL prover for description logic
(as efficient as DL-specific tools!)
Look at PROSPER toolkit
consistency: see IJCAR-workshop on non-provability in Cork
IJCAR workshop about logical frameworks and meta-languages
Integrate CCC
Encodings
Errors:
Test suite (Christian's mail)
Klaus' wayfinding example
UniForM workbench:
first steps towards CASL instance, using ATerms and re-using MMISS instance
variants for specs (needed for DOLCE: CASL variant, DL variant, ...)
Integration of MAYA and Isabelle/HOL (global HOL-Coding of
Grothendieck logic)
+ for TAS: reflection of HOL in HOL, to be composed with encodings
(i.e. signatures, axioms, signature morphisms in HOL,
re-use ML signatures) (Einar)
Display Specs as daVinci subgraphs
User interface
--------------
Logic graph window
Input text window
Development graph window
Prover windows
************************************************
FOR STUDENTS
************************************************
Emacs mode
Hets Web interface (cf. CATS/web_interface2.sml)
CCC ?
Packaging of installation
integrate QuickCheck
XML interface
GUI (vgl. VSE)
increase performance
++++++++++++++++++++++++++++++++++++++++++++++++
Remaining things
++++++++++++++++++++++++++++++++++++++++++++++++
Mark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
Coq, PTT in Maude
Proof general interface (1 day)
Test Maya with basic datatypes
Verbesserung der Fehlermeldungen
Improve encoding: CATS/basic_encode.sml (3 days)
More HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
Renamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
Example of Agnes und Frank: proofs in HOL-CASL (2 days)
Term input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
Examples for cond rewriting -> Christophe
Doku: VSE-Prover, VSE-Method VSE-demo in Bremen?
Adapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
Eigene IsaWin-Instanz mit CASL-RS statt HOL-RS
HOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
HOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
HOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
Encoding of structured free (3 days)
Encoding of structured cofree (2 weeks)
Eingabesyntax als Mix zwischen CASL und HOL (3 days)
Adapt Isabelle unions to CASL unions (1 week)
IsaWin git/src/isa_ext/casl_thy.sml (1 week)
Generate Proof obligations (1 week)
Add renaming to Isabelle kernel (2 months)
Basic datatypes CASL-lib/Basic/basic.casl
Repository mit korrekten und fehlerhaften Specs
HetCATS User manual, Doku fuer Environments (2 weeks)
Conversion ASF/SDF-Parser -> abstract syntax (in Haskell)
Comparsion of parsers (ML-yacc parser, SDF-Parser)
Conversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
PVS anbinden (Kooperation mit Cachan?)
Portations: Intel-Solaris, Mac OS-10 (2 weeks)
(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
Views on CASL specs: CATS/viewer.sml (2 weeks)
Uebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
Module graph CATS/module_graph.sml (1 week) -> Maya?
ATerms via XML: CATS/aterms.sml (2 weeks)
Neues Tool-Schaubild auf Web-Seiten ver�ffentlichen
Library management: CATS/lib_ana.sml (2 weeks)
Version management/Uniform Workbench: CATS/lib_ana.sml (2 months)
{- This does not work due to needed ordering:
instance Functor Set where
fmap = mapSet
instance Monad Set where
return = unitSet
m >>= k = unionManySets (setToList (fmap k m))
-}