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
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellAs a prerequisite for change management, a dependency tracking
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellrelation is needed. Each theory morphism and each (theoroidal)
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell(co)morphism (see also ticket #172) leads to a tracking relation
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellbetween the symbols and axioms of the source and the target
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellsignature/theory. The intended semantics is that tr(sy1,sy2) means
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellthat sy2 is contained in the entity that is the image of symbol
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellsy1. For example, a function symbol may be mapped (by a comorphism) to
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnelltwo function symbols, or to one function symbol and an axiom.
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellImportant properties:
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellChange management tracks which symbols and axioms are needed to
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellprove a specific theorem. These symbols and axioms then can,
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellvia the tracking relation, also be traced back to their origin.
c299abfd457a72f3b93d443fe40ad36169e1c0a8Craig McDonnellIf in the changed development graph, they are still there, then
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellthen the proof is still valid.
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellEntities on the abstract level
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell------------------------------
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell- Objects = symbols? what are objects? all subterms? symbols are those entities that can be mapped in a signature morphism
dd00389f072a764f2afbb218de7cf9fd60baf119Phill Cunnington- Theories / signatures
dd00389f072a764f2afbb218de7cf9fd60baf119Phill Cunnington- object is contained in statement, theory
dd00389f072a764f2afbb218de7cf9fd60baf119Phill Cunnington- theory is made of signature and statements
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell- signature is made of symbols??? This would lead to "subsort symbols" etc.
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell- 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
dd00389f072a764f2afbb218de7cf9fd60baf119Phill Cunningtontyping. 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.
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell=================
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellCASL methodology, 3rd volume, ccc tools (Till, Lutz, Cxl)
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellCoCASL/Concurrent Haskell (George's events)/SPIN/CspCASL (Till, Shi, Lutz)
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell Modal-CASL als Anforderungssprache
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell div. Prozessalgebren (wir stellen den allg. Rahmen)
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellAbstract robotics (cxl, paolo)
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellAWE II / General FM (cxl, bkb)
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell(2) Expose commutativity in tool chains. It is certainly usefull to get
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnelloverviews of tool compositions. However, what happened with proven techniques
9f2dfcd449ae1cfd1bcc249ef5aec29950cf3fc7Phill Cunningtonto do this like T-diagrams? They were first described in
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellJay Earley , Howard Sturgis, A formalism for translator interactions,
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellCommunications of the ACM, v.13 n.10, p.607-617, Oct. 1970
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell[doi>10.1145/355598.362740]
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellPopular accounts are:
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellhttp://proglang.informatik.uni-freiburg.de/teaching/compilerbau/2004/T-diagrams.pdf
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellA modified version can be found in:
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell@article{197336,
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellauthor = {Andrew W. Appel},
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnelltitle = {Axiomatic bootstrapping: a guide for compiler hackers},
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnelljournal = {ACM Trans. Program. Lang. Syst.},
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellvolume = {16},
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellyear = {1994},
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellissn = {0164-0925},
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellpages = {1699--1718},
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnelldoi = {http://doi.acm.org/10.1145/197320.197336},
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnellpublisher = {ACM},
c299abfd457a72f3b93d443fe40ad36169e1c0a8Craig McDonnelladdress = {New York, NY, USA},
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell- theory morphisms (cxl)
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell- Latin2: Mizar->Isabelle, PVS->Isabelle
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell Joe Hurd (binary format for HOL) PLMMS 09
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell Cezary Kaliszyk (HOL import)
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell Klaus Grue LogiWeb
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell- Isabelle parser
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell terms of basic logic, annotated with datatypes etc.
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell - source+markup (locales, non-logical stuff, ...)
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell - code_gen (Haftmann) intermediate language, Haskell-like
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell datatype, function, etc., useful for translation to Haskell etc.
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell - in parallel: find_theorems (leave alone concealed theorems)
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell -> additional theorems
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell how is HOL.plus specified?
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell unknown (axiomatic)
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell equiontional (fun, primrec)
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell inductive (relational)
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell - logical foundation: types, consts (typeclasses, sorts), thms
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell- LF coding? Isabelle as a LF for Hets
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell- nice view on tool-generated Isabelle theories
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell - either fancy syntax rules
cf7084cf20623b8a2d7da2cc101288f2cf516d67Craig McDonnell - or (better) annotated source
- model finders (e.g. nitpick, quickcheck) Lukas Bulwahn, Jasmin Blanchette (Vortrag CADE)