hets.bib revision 2c66eeb1cc9ad264525901f10c35c66638f91865
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
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski author = {L. Schr\"oder and T. Mossakowski and C. Maeder},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski title = {{\HasCASL} -- {I}ntegrated functional specification and programming. {L}anguage Summary},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski note = {Available at \verb?http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/? \verb?CoFI/HasCASL?}},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski year = {2003},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski@Article{Schroder05b,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski author = {Lutz Schr{\"o}der},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski title = {The {HasCASL} Prologue - Categorical Syntax and Semantics of the Partial {$\lambda$}-calculus},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski year = {2006},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski journal = {Theoret. Comput. Sci.},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski volume = {353},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski pages = {1-25},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski keywords = {partial lambda-calculus partial cartesian closed category Henkin model HasCASL CASL},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski pdfurl = {http://www.informatik.uni-bremen.de/~lschrode/hascasl/prologue.pdf},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski psurl = {http://www.informatik.uni-bremen.de/~lschrode/hascasl/prologue.ps},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski abstract = {We develop the semantic foundations of the specification language HasCASL, which combines algebraic specification and functional programming on the basis of Moggi's partial {$\lambda$}-calculus. Generalizing Lambek's classical equivalence between the simply typed {$\lambda$}-calculus and cartesian closed categories, we establish an equivalence between partial cartesian closed categories (pccc's) and partial {$\lambda$}-theories. Building on these results, we define (set-theoretic) notions of intensional Henkin model and syntactic {$\lambda$}-algebra for Moggi's partial {$\lambda$}-calculus. These models are shown to be equivalent to the originally described categorical models in pccc's via the global element construction. The semantics of HasCASL is defined in terms of syntactic {$\lambda$}-algebras. Correlations between logics and classes of categories facilitate reasoning both on the logical and on the categorical side; as an application, we pinpoint unique choice as the distinctive feature of topos logic (in comparison to intuitionistic higher-order logic of partial functions, which by our results is the logic of pccc's with
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiequality). Finally, we give some applications of the model-theoretic equivalence result to the semantics of HasCASL and its relation to first-order CASL.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski status = {Reviewed}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski@unpublished{Schroder-habil,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski author = {Lutz Schr�der},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski title = {Higher order and reactive algebraic specification and development},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski school = {University of Bremen},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski year = {2005},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski note = {summary of papers constituting a cumulative habilitation thesis; available under \url{http://www.informatik.uni-bremen.de/~lschrode/papers/Summary.pdf}},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski@Misc{ModalCASL,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski author = {T. Mossakowski},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski title = {Modal{CASL} - Specification with Multi-Modal Logics. Language Summary},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski year = {2004},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski keywords = {modal logic CASL},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski pdfurl = {http://www.tzi.de/~till/papers/Modal-Summary.pdf},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski psurl = {http://www.tzi.de/~till/papers/Modal-Summary.ps},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski abstract = {ModalCASL extends CASL by modal operators. Syntax for ordinary
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski modalities, multi-modal logics as well as term-modal
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski logic (also covering dynamic logic) is provided.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski Specific modal logics can be obtained via restrictions to
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski sublanguages.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiThis document provides a detailed definition of the ModalCASL syntax
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiand an informal description of the semantics, building on the existing
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCASL Summary.},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski status = {Other}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@article{RiazanovV02,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski author = {Alexandre Riazanov and
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Andrei Voronkov},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski title = {The design and implementation of {VAMPIRE}},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski journal = {AI Communications},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski volume = {15},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski number = {2-3},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski year = {2002},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski pages = {91-110},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ee = {http://iospress.metapress.com/openurl.asp?genre=article{\&}issn=0921-7126{\&}volume=15{\&}issue=2{\&}spage=91},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski bibsource = {DBLP, http://dblp.uni-trier.de}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@InProceedings{ZimmerAutexier06,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiauthor = {J{\"u}rgen Zimmer and Serge Autexier},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskititle = {The {M}ath{S}erve {S}ystem for {S}emantic {W}eb {R}easoning {S}ervices},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskibooktitle = {3rd IJCAR},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskieditor = {U. Furbach and N. Shankar},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiseries = {LNCS 4130},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskipublisher = {Springer},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@InProceedings{LuettichEA06a,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski author = {Klaus L{\"u}ttich and Till Mossakowski},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski title = {Reasoning {S}upport for {CASL} with {A}utomated {T}heorem {P}roving {S}ystems},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski note = {WADT 2006, Springer LNCS, to appear},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski status = {Other}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@article{Mossakowski02,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski author = {Till Mossakowski},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski title = {Relating {\CASL} with Other Specification Languages:
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski the Institution Level},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski journal = {Theoretical Computer Science},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski volume = {286},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski pages = {367--475},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@ARTICLE{GoguenBurstall92,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiAUTHOR = "J. A. Goguen and R. M. Burstall",
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiTITLE = "Institutions: Abstract Model Theory for Specification and
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiJOURNAL = "Journal of the Association for Computing Machinery",
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiPAGES = {95--146},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiNOTE = {Predecessor in: LNCS 164, 221--256, 1984.},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@article{GoguenRosu02,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski author = {J. Goguen and G. Ro\c{s}u},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski title = {Institution morphisms},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski journal = {Formal aspects of computing},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski volume = {13},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski year = {2002},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski pages = {274-307},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@unpublished{Habil,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Author = {T. Mossakowski},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Title = {Heterogeneous specification and the heterogeneous tool set},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Note = {Habilitation thesis, University of Bremen},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@InProceedings{MossakowskiEA06,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski author = {Till Mossakowski and Christian Maeder and Klaus L{\"u}ttich},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski title = {The {H}eterogeneous {T}ool {S}et},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski year = {2007},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski editor = {Orna Grumberg and Michael Huth},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski booktitle = {TACAS 2007},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski publisher = {Springer-Verlag Heidelberg},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski series = {Lecture Notes in Computer Science},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski volume = {4424},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski pages = {519-522},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski keywords = {proof heterogeneity logic institution prover theorem integration development graph},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski pdfurl = {http://www.tzi.de/~till/papers/hets-tacas-toolpaper.pdf},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski psurl = {http://www.tzi.de/~till/papers/hets-tacas-toolpaper.ps},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski abstract = {Heterogeneous specification becomes more and more important because
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskicomplex systems are often specified using multiple viewpoints,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiinvolving multiple formalisms. Moreover, a formal software development
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiprocess may lead to a change of formalism during the development.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiHowever, current research in integrated formal methods only deals
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiwith ad-hoc integrations of different formalisms.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThe heterogeneous tool set (Hets) is a parsing, static analysis and
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiproof management tool combining various such tools for individual
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskispecification languages, thus providing a tool for heterogeneous
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskimulti-logic specification. Hets is based on a graph of logics and
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskilanguages (formalized as so-called institutions), their tools, and
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskitheir translations. This provides a clean semantics of heterogeneous
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskispecification, as well as a corresponding proof calculus. For proof
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskimanagement, the calculus of development graphs (known from other
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskilarge-scale proof management systems) has been adapted to
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiheterogeneous specification. Development graphs provide an overview of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskithe (heterogeneous) specification module hierarchy and the current
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiproof state, and thus may be used for monitoring the overall
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskicorrectness of a heterogeneous development.},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski status = {Reviewed}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@Article{MossakowskiEtAl05,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski author = {T. Mossakowski and S. Autexier and D. Hutter},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski title = {Development Graphs -- Proof Management for Structured Specifications},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski year = {2006},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski journal = {Journal of Logic and Algebraic Programming},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski volume = {67},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski pages = {114-145},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski number = {1-2},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski keywords = {development graph proof logic institution completeness},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski url = {http://www.sciencedirect.com/science?_ob=GatewayURL&_origin=CONTENTS&_method=citationSearch&_piikey=S1567832605000810&_version=1&md5=7c18897e9ffad42e0649c6b41203f41e},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski psurl = {http://www.tzi.de/~till/papers/dgh_journal.ps},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski abstract = {Development graphs are a tool for dealing with structured
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski specifications in a formal program development in order to ease the
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski management of change and reusing proofs. In this work, we extend
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski development graphs with hiding (e.g. hidden operations). Hiding is
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski a particularly difficult to realize operation, since it does not
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski admit such a good decomposition of the involved specifications as
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski other structuring operations do. We develop both a semantics and
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski proof rules for development graphs with hiding. The rules are proven
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski to be sound, and also complete relative to an oracle for
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski conservative extensions. We also show that an absolutely complete set
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski of rules cannot exist.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski The whole framework is developed in a way independent of the
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski underlying logical system (and thus also does not prescribe the
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski nature of the parts of a specification that may be hidden). We also
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski show how various other logic independent specification formalisms
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski can be mapped into development graphs; thus, development graphs can
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski serve as a kernel formalism for management of proofs and of change.},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski issn = {1567-8326},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski status = {Reviewed}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@Book{blackburn_p-etal:2001a,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski author = "Patrick BLackburn and Maarten de Rijke and Yde
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski title = "Modal Logic",
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski publisher = "Cambridge University Press",
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski year = "2001",
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski address = "Cambridge, England",
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ISBN = "0 521 52714 7 (pbk)",
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski topic = "modal-logic;",
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski@unpublished{TorriniEtAl07,
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski author = {Paolo Torrini and Christoph L\"{u}th and
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski Christian Maeder and Till Mossakowski},
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski title = {Translating Haskell to Isabelle},
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski note = {submitted for publication},
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski@MastersThesis{Groening05,
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski author = {Sonja Gr\"{o}ning},
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski title = {Beweisunterst\"{u}tzung f\"{u}r HasCASL in Isabelle
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski school = {University of Bremen},
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski note = {Diplomarbeit},
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski year = {2005},