todo revision 2d76902bf3b380a32268ccc0d2cd9e376988a060
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringPlan and priority list for CoFI tool activities
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringDiplom: Encoding for HasCASL in Isabelle/HOL(CF)
5430f7f2bc7330f3088b894166bf3524a067e3d8Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringdevelopment graph calculus
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering- Stack overflow for "show just subtree"
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering- view-test7.casl should be provable with globDecomp + locDecopm
5430f7f2bc7330f3088b894166bf3524a067e3d8Lennart Poettering- fail when doing first globDecomp, then local decomp in RelationsAndOrders
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering- correct MAYA: glob decomp: some links are not found (Jorina)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringtype check for CASL
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering*** Error encode.casl:8.30, No correct typing for
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringport CCC to Haskell
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringFunktionen imageOfMorphism und inhabited
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering mit "cvs add SigFuns.hs" einchecken
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering"free datatypes and recursive equations are consistent"
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringcheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringJust True => Yes, is consistent
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringJust False => No, is inconsistent
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringNothing => don't know
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringcall the symbols in the image of the signature morphism "new"
1fd961211df69ce672252d543bf4777738647048Zbigniew Jędrzejewski-Szmek- each new sort must be a free type,
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek i.e. it must occur in a sort generation constraint that is marked as free
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek (Sort_gen_ax constrs True)
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek if not, output "don't know"
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek and there must be one term of that sort (inhabited)
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek if not, output "no"
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek- group the axioms according to their leading operation/predicate symbol,
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek i.e. the f resp. the p in
1fd961211df69ce672252d543bf4777738647048Zbigniew Jędrzejewski-Szmek forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Implication Application Strong_equation
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Implication Predication Equivalence
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering if there are axioms not being of this form, output "don't know"
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
9f7dad774ebfad23269800b7096eaad087481debVille SkyttäZicheng (Till)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringTranslation from CASL with partiality to CASL without partiality
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringdetails: see paper in Theoretical Computer Science, p. 418
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart Poettering************************************************
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart Poettering************************************************
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart PoetteringWrite web interface for Hets
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringsee the web interface for Cats:
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringhttp://www.informatik.uni-bremen.de/cgi-bin/cats.cgi
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering-------------------------------------------------------------------
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringLaTeX pretty printer
04ac799283f517672a5424e7c5bf066cfa4ca020Zbigniew Jędrzejewski-Szmeka) analysierte Formeln und Terme optimal/k�rzer ausgeben:
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringshorten :: Sign -> {TERM, FORMULA} -> {TERM, FORMULA}
4d62fb4298a5904a53f484636c91540d08f68765Lennart PoetteringIn Abh�ngigkeit von Sign werden z.B. nicht-�berladene Funktionen
04ac799283f517672a5424e7c5bf066cfa4ca020Zbigniew Jędrzejewski-Szmekunqualifiziert ausgeben bzw. zwecks Eindeutigkeit wird (minimal) nur
4d62fb4298a5904a53f484636c91540d08f68765Lennart Poetteringmit dem Ergebnistyp qualifiziert.
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering((a: Nat) + (b: Nat)): Nat
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poetteringb) eine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringund andere Formate besser zu unterst�tzen und einheitlichen PP code
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringf�r die CASL Datentypen zu bekommen.
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringHasCASL hat auch noch keine Mixfix- und Latex Ausgabe.
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringHaskell modules: hiding, renaming
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering- group the axioms according to their leading operation/predicate symbol,
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering i.e. the f resp. the p in
04d39279245834494baccfdb9349db8bf80abd13Lennart Poettering forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
04d39279245834494baccfdb9349db8bf80abd13Lennart Poettering forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
04d39279245834494baccfdb9349db8bf80abd13Lennart Poettering if there are axioms not being of this form, output error
9980033377c105d2cd6539c9d73ee61d4c2263b0Lennart PoetteringMissing points for heterogeneous WADT 04 example:
9980033377c105d2cd6539c9d73ee61d4c2263b0Lennart Poettering- improve display of HasCASL sigs + mors
9980033377c105d2cd6539c9d73ee61d4c2263b0Lennart PoetteringStatic analysis for HasCASL
f8964235e69f58225dec378437b1789744cd22a9Lennart Poettering checking class constraints of terms
f8964235e69f58225dec378437b1789744cd22a9Lennart Poettering pattern analysis for program equations
fb69ed55e5f8e82145440ba15075e8db807bf7faMichael Biebl - for simple types (currently type synonyms)
f8964235e69f58225dec378437b1789744cd22a9Lennart Poettering symbol representation
f8964235e69f58225dec378437b1789744cd22a9Lennart Poettering symbol map analysis (hiding sub/supertypes)
f8964235e69f58225dec378437b1789744cd22a9Lennart PoetteringWeak amalgamation analysis?
77b6e19458f37cfde127ec6aa9494c0ac45ad890Lennart PoetteringInstantiate Transformation Application system for HasCASL?
77b6e19458f37cfde127ec6aa9494c0ac45ad890Lennart PoetteringAutomatic generation of Haskell (for a HasCASL subset)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringProofs in HasCASL
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek************************************************
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek************************************************
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmekvisualization of "taxonomy" of CASL signatures
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek (subsorts = inheritance, unary preds = concepts, binary preds = relations)
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-SzmekRecognize guarded fragment of CASL:
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek G ::= forall x . At(x) => G where At is a conjunction of atoms
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek | exists x . At(x) /\ G
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-SzmekJoost Visser wg. ATerms in Haskell => neues Repository
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
a41fe3a29372f8e6c4e7733bf85940a023811301Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringBeweise in Isabelle
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringCASL consistency checker
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering (Vorbild: Larch-Handbuch)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
acbeb42770e1e99955ebc4464a0439cf741b3aebZbigniew Jędrzejewski-SzmekParser and static analysis for CSP-CASL
acbeb42770e1e99955ebc4464a0439cf741b3aebZbigniew Jędrzejewski-Szmek************************************************
acbeb42770e1e99955ebc4464a0439cf741b3aebZbigniew Jędrzejewski-Szmek************************************************
acbeb42770e1e99955ebc4464a0439cf741b3aebZbigniew Jędrzejewski-SzmekCASL consistency checker
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringIsaWin: support CASL-libraries
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering************************************************
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering************************************************
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringStatic analysis of architectural specs
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering************************************************
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering************************************************
ab1f063390f55e14a8de87f21c4fad199eb908a6Lennart PoetteringCASL2PCFOL: x_i -> t_i, t=[inj(x_i)]
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringpacking of binaries: add hets-update, refer to TclTk
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringtest for sublogic before applying comorphism
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringavoid cyclic comorphisms
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringMissing points for heterogeneous WADT 04 example:
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poettering- coding to Isabelle: translate sort gen constraints
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poettering- extended globDecomp rule: existing local Thm links
a7f5bb1eafadbb08c8528baae588bbe773a37e79William Giokas (e.g. generated by %implied) should lead to fewer new local
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poettering links ("local composition" rule)
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poettering- Improve adapation to Isabelle's lexis
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart PoetteringIsabelle: (ask Christoph)
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering free datatypes
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering prove local thm link (=> green)
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering "prove" menu with choice windows
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering incorporate sublogics
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek sublogic translation table
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poettering better interaction between Isabelle instance (for one node)
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil + selection of single goals that are proved
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart Poettering => use PGIP interface (Christoph, David)
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil correct show theory
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil Keep proofs and lemmas in .thy files (kind of merge)
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil CASL-like syntax
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil CASL annotation for lemmas that should be used in proof
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil inherit CASL's mixfix syntax
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal VyskocilSignatures versus theories: where to store additional infos?
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocilcomp(id,x)=x for comorphism names
7027ff61a34a12487712b382a061c654acc3a679Lennart PoetteringGeneralise CASL2Modal
7027ff61a34a12487712b382a061c654acc3a679Lennart PoetteringMixfix analysis + typecheck for modality axiomatizations
7027ff61a34a12487712b382a061c654acc3a679Lennart PoetteringModal logics: modal logic, temporal logic, mu calculus
7027ff61a34a12487712b382a061c654acc3a679Lennart Poettering+ translations (e.g. modal to FOL)
7027ff61a34a12487712b382a061c654acc3a679Lennart PoetteringCASL->Haskell with free DTs (mark sortgens) + recursion
7027ff61a34a12487712b382a061c654acc3a679Lennart PoetteringCoding of subsorts as unary predicates (for ontologies)
7027ff61a34a12487712b382a061c654acc3a679Lennart PoetteringTranslation between Achim's ontology data structure and CASL (in Hets)
79640424059328268b9fb6c5fa8eb777b27a177eJan Engelhardt- List[Dec] wird List[Pos]
7027ff61a34a12487712b382a061c654acc3a679Lennart Poettering- George wg. Schlie�en von Fenstern
7027ff61a34a12487712b382a061c654acc3a679Lennart Poettering- node numbers do not match
7027ff61a34a12487712b382a061c654acc3a679Lennart Poettering- thm links with external target should be provable as well
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart PoetteringRemove warnings
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart PoetteringDifferent types of logic translations
e9dd9f9547350c7dc0473583b5c2228dc8f0ab76Jason St. JohnImprove Static analysis of structured specs
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart PoetteringDevelopment graph calculus, Strategies for DG rules
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart PoetteringManagement of change
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart PoetteringIntegrate provers
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering Otter model checker
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering FOL-prover by Uli Furhbach
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering Isabelle codings: www.inf.ethz.ch/~vigano
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering Renate Schmidt, Manchester: uses FOL prover for description logic
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering (as efficient as DL-specific tools!)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering Look at PROSPER toolkit
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering consistency: see IJCAR-workshop on non-provability in Cork
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering IJCAR workshop about logical frameworks and meta-languages
ff01d048b4c1455241c894cf7982662c9d28fd34Lennart PoetteringKlaus' wayfinding example
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringUniForM workbench:
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poetteringfirst steps towards CASL instance, using ATerms and re-using MMISS instance
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poetteringvariants for specs (needed for DOLCE: CASL variant, DL variant, ...)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringIntegration of MAYA and Isabelle/HOL (global HOL-Coding of
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering Grothendieck logic)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering + for TAS: reflection of HOL in HOL, to be composed with encodings
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom Gundersen (i.e. signatures, axioms, signature morphisms in HOL,
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering re-use ML signatures) (Einar)
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart PoetteringDisplay Specs as daVinci subgraphs
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart PoetteringLogic graph window
a41fe3a29372f8e6c4e7733bf85940a023811301Lennart PoetteringInput text window
a41fe3a29372f8e6c4e7733bf85940a023811301Lennart PoetteringDevelopment graph window
aa28aefe61c5406c5cb631f3e82457b6d1bcc967Lennart Poettering************************************************
aa28aefe61c5406c5cb631f3e82457b6d1bcc967Lennart Poettering************************************************
aa28aefe61c5406c5cb631f3e82457b6d1bcc967Lennart PoetteringHets Web interface (cf. CATS/web_interface2.sml)
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart PoetteringPackaging of installation
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart Poetteringintegrate QuickCheck
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart Poetteringincrease performance
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart Poettering++++++++++++++++++++++++++++++++++++++++++++++++
aa28aefe61c5406c5cb631f3e82457b6d1bcc967Lennart PoetteringRemaining things
aa28aefe61c5406c5cb631f3e82457b6d1bcc967Lennart Poettering++++++++++++++++++++++++++++++++++++++++++++++++
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringMark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering Coq, PTT in Maude
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringProof general interface (1 day)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringTest Maya with basic datatypes
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringVerbesserung der Fehlermeldungen
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringImprove encoding: CATS/basic_encode.sml (3 days)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringMore HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringRenamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringExample of Agnes und Frank: proofs in HOL-CASL (2 days)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringTerm input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringExamples for cond rewriting -> Christophe
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringDoku: VSE-Prover, VSE-Method VSE-demo in Bremen?
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringAdapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
bc2f673ec24b59948fcfc35b3077fda0314e69d8Lennart PoetteringEigene IsaWin-Instanz mit CASL-RS statt HOL-RS
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom GundersenHOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom GundersenHOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom GundersenHOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom GundersenEncoding of structured free (3 days)
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom GundersenEncoding of structured cofree (2 weeks)
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom GundersenEingabesyntax als Mix zwischen CASL und HOL (3 days)
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom GundersenAdapt Isabelle unions to CASL unions (1 week)
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom GundersenGenerate Proof obligations (1 week)
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom GundersenAdd renaming to Isabelle kernel (2 months)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringRepository mit korrekten und fehlerhaften Specs
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringHetCATS User manual, Doku fuer Environments (2 weeks)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringConversion ASF/SDF-Parser -> abstract syntax (in Haskell)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringComparsion of parsers (ML-yacc parser, SDF-Parser)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringConversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringPVS anbinden (Kooperation mit Cachan?)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringPortations: Intel-Solaris, Mac OS-10 (2 weeks)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringViews on CASL specs: CATS/viewer.sml (2 weeks)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringUebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringModule graph CATS/module_graph.sml (1 week) -> Maya?
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringATerms via XML: CATS/aterms.sml (2 weeks)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringNeues Tool-Schaubild auf Web-Seiten ver�ffentlichen
bc2f673ec24b59948fcfc35b3077fda0314e69d8Lennart PoetteringLibrary management: CATS/lib_ana.sml (2 weeks)
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart PoetteringVersion management/Uniform Workbench: CATS/lib_ana.sml (2 months)
e9dd9f9547350c7dc0473583b5c2228dc8f0ab76Jason St. John{- This does not work due to needed ordering:
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poetteringinstance Functor Set where
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poetteringinstance Monad Set where
88d04e31ce0837ebf937ab46c3c39a0d93ab4c7cLennart Poettering return = unitSet
88d04e31ce0837ebf937ab46c3c39a0d93ab4c7cLennart Poettering m >>= k = unionManySets (setToList (fmap k m))
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart PoetteringAufbau von comptable
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering--------------------
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering[("normal","normal","normal"),
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering ("normal","inclusion","normal"),
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering ("inclusion","normal","normal"),
88d04e31ce0837ebf937ab46c3c39a0d93ab4c7cLennart Poettering ("inclusion","inclusion","inclusion")]
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart PoetteringAufbau von ginfo
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart Poettering--------------------
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart PoetteringMit initgraphs erzeugen
39ed67d14694983dabd6641c02216aa440eed767Lennart PoetteringAufbau des Graphen selbst
39ed67d14694983dabd6641c02216aa440eed767Lennart Poettering------------------------