todo revision e539b8cb4a47f987bc57c90ee964219ac53841ff
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
Plan and priority list for CoFI tool activities
************************************************
Sonja (Till)
************************************************
Haskell parser f�r XHaskell erweitern
Dimplom: Encoding for HasCASL in Isabelle/HOL(CF)
************************************************
Jorina (Till)
************************************************
development graph calculus
************************************************
Martin (Till)
************************************************
type check for CASL
if a subterm is not typeable at all, output it
************************************************
Mingyi (Till)
************************************************
gmake packages
make hets
try out small examples, e.g.
export HETS_LIB=.../CASL-lib
hets .../CASL-lib/Basic/Algebra_I.casl
look at HetCATS/README
Test auf Einpunkt-Modell
(ein Datenelement, wahre Pr�dikate, totale Funktionen)
siehe ccc/OnePoint.hs
port CCC to Haskell
************************************************
Zicheng (Till)
************************************************
************************************************
Heng (Klaus)
************************************************
LaTeX pretty printer
************************************************
Christian
************************************************
Sprachdesign HasCASL
Verh�ltnis von Parametrisierung und Polymorphie/Typklassen
Static analysis for HasCASL
Subsorting
Symbol map analysis
Weak amalgamation analysis
Instantiate Transformation Application system for HasCASL
Automatic generation of Haskell (for a HasCASL subset)
Proofs in HasCASL
Case study
S�nke Magnussen kontaktieren (der arbeitet mit Has-CASL-�hnlicher Sprache)
************************************************
Klaus
************************************************
visualization of "taxonomy" of CASL signatures
(subsorts = inheritance, unary preds = concepts, binary preds = relations)
Recognize guarded fragment of CASL:
G ::= forall x . At(x) => G where At is a conjunction of atoms
| exists x . At(x) /\ G
Joost Visser wg. ATerms in Haskell => neues Repository
************************************************
Markus, Lutz
************************************************
Beweise in Isabelle
CASL consistency checker
Weitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
(Vorbild: Larch-Handbuch)
Simpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
Parser and static analysis for CSP-CASL
************************************************
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))
-}