ideas revision 3881c469ed14d0bc1974c2a15e396b83ca16f5c0
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
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill MossakowskiAs a prerequisite for change management, a dependency tracking
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskirelation is needed. Each theory morphism and each (theoroidal)
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowski(co)morphism (see also ticket #172) leads to a tracking relation
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskibetween the symbols and axioms of the source and the target
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskisignature/theory. The intended semantics is that tr(sy1,sy2) means
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskithat sy2 is contained in the entity that is the image of symbol
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskisy1. For example, a function symbol may be mapped (by a comorphism) to
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskitwo function symbols, or to one function symbol and an axiom.
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill MossakowskiImportant properties:
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill MossakowskiChange management tracks which symbols and axioms are needed to
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskiprove a specific theorem. These symbols and axioms then can,
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskivia the tracking relation, also be traced back to their origin.
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill MossakowskiIf in the changed development graph, they are still there, then
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskithen the proof is still valid.
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill MossakowskiEntities on the abstract level
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowski------------------------------
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowski- Objects = symbols? what are objects? all subterms? symbols are those entities that can be mapped in a signature morphism
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowski- Theories / signatures
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowski- object is contained in statement, theory
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowski- theory is made of signature and statements
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowski- signature is made of symbols??? This would lead to "subsort symbols" etc.
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowski- Statement is made of objects??? This would lead to parchments. Logics have to specify something like an XML schema, such that we can look into the abstract syntax tree of all entities. However, this has no logical meaning. Then, we can also OMDocify things and use variables, constants, application, binders, with
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskityping. Again, the logical important thing is the tracking relation. Provide this feature only for OmDoc-based formalisms? Or make it into a general design principle (hard migration!). Structured presentation of statements does not lead to logical decomposition. Rather, the statement is computed and then treated as if it were an atomic object in the target theory.
8793c68e374ef07d13eac84293d351ab46f47047Till Mossakowski=================
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 MossakowskiAbstract robotics (cxl, paolo)
f3a84cc409ed345569be6673d05072dcb4291ebeTill MossakowskiAWE II / General FM (cxl, bkb)
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowski(2) Expose commutativity in tool chains. It is certainly usefull to get
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskioverviews of tool compositions. However, what happened with proven techniques
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskito do this like T-diagrams? They were first described in
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill MossakowskiJay Earley , Howard Sturgis, A formalism for translator interactions,
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill MossakowskiCommunications of the ACM, v.13 n.10, p.607-617, Oct. 1970
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowski[doi>10.1145/355598.362740]
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill MossakowskiPopular accounts are:
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskihttp://proglang.informatik.uni-freiburg.de/teaching/compilerbau/2004/T-diagrams.pdf
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill MossakowskiA modified version can be found in:
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowski@article{197336,
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskiauthor = {Andrew W. Appel},
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskititle = {Axiomatic bootstrapping: a guide for compiler hackers},
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskijournal = {ACM Trans. Program. Lang. Syst.},
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskivolume = {16},
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskiyear = {1994},
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskiissn = {0164-0925},
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskipages = {1699--1718},
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskidoi = {http://doi.acm.org/10.1145/197320.197336},
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskipublisher = {ACM},
5e47bbd77c4d8dfc224acce06af5fb3ee1a562cfTill Mossakowskiaddress = {New York, NY, USA},
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski- theory morphisms (cxl)
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski- Latin2: Mizar->Isabelle, PVS->Isabelle
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski Joe Hurd (binary format for HOL) PLMMS 09
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski Cezary Kaliszyk (HOL import)
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski Klaus Grue LogiWeb
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski- Isabelle parser
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski terms of basic logic, annotated with datatypes etc.
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski - source+markup (locales, non-logical stuff, ...)
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski - code_gen (Haftmann) intermediate language, Haskell-like
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski datatype, function, etc., useful for translation to Haskell etc.
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski - in parallel: find_theorems (leave alone concealed theorems)
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski -> additional theorems
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski how is HOL.plus specified?
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski unknown (axiomatic)
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski equiontional (fun, primrec)
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski inductive (relational)
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski - logical foundation: types, consts (typeclasses, sorts), thms
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski- LF coding? Isabelle as a LF for Hets
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski- nice view on tool-generated Isabelle theories
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski - either fancy syntax rules
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski - or (better) annotated source
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski- using PIDE for Hets (asynchronous editing - checking - proving)
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski- Ubuntu package
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski- isomorphism theorems
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski- HOL-light to Isabelle. Descision procedures?
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski- model finders (e.g. nitpick, quickcheck) Lukas Bulwahn, Jasmin Blanchette (Vortrag CADE)
3881c469ed14d0bc1974c2a15e396b83ca16f5c0Till Mossakowski- default simpset and claset setup