Evgenii Akentev
·
2019-01-18
thesis.bib
1@article{DBLP:journals/corr/DragoniGLMMMS16,
2 author = {Nicola Dragoni and
3 Saverio Giallorenzo and
4 Alberto Lluch{-}Lafuente and
5 Manuel Mazzara and
6 Fabrizio Montesi and
7 Ruslan Mustafin and
8 Larisa Safina},
9 title = {Microservices: yesterday, today, and tomorrow},
10 journal = {CoRR},
11 volume = {abs/1606.04036},
12 year = {2016},
13 url = {http://arxiv.org/abs/1606.04036},
14 timestamp = {Sat, 02 Jul 2016 18:16:28 +0200},
15 biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/DragoniGLMMMS16},
16 bibsource = {dblp computer science bibliography, http://dblp.org}
17}
18
19@article{Kumar:2014:CVI:2578855.2535841,
20 author = {Kumar, Ramana and Myreen, Magnus O. and Norrish, Michael and Owens, Scott},
21 title = {CakeML: A Verified Implementation of ML},
22 journal = {SIGPLAN Not.},
23 issue_date = {January 2014},
24 volume = {49},
25 number = {1},
26 month = jan,
27 year = {2014},
28 issn = {0362-1340},
29 pages = {179--191},
30 numpages = {13},
31 url = {http://doi.acm.org/10.1145/2578855.2535841},
32 doi = {10.1145/2578855.2535841},
33 acmid = {2535841},
34 publisher = {ACM},
35 address = {New York, NY, USA},
36 keywords = {ML, compiler bootstrapping, compiler verification, machine code verification, read-eval-print loop, verified garbage collection., verified parsing, verified type checking},
37}
38
39@MastersThesis{montesi2010jolie,
40 author = "Fabrizio Montesi",
41 title = "{J}{O}{L}{I}{E}: a {S}ervice-oriented {P}rogramming {L}anguage",
42 school = "University of Bologna",
43 year = {2010},
44 url = {\url{http://www.fabriziomontesi.com/files/m10.pdf}}
45}
46
47@article{nielsen2013type,
48 title={A type system for the jolie language},
49 author={Nielsen, Julie Meinicke},
50 journal={Technical University of Denmark Informatics and Mathematical Modelling},
51 year={2013}
52}
53
54@online{agdastdlib,
55 title = {The {Agda} standard library},
56 howpublished = {\url{https://github.com/agda/agda-stdlib}}
57}
58
59@inproceedings{bove,
60 author = {Bove, Ana and Dybjer, Peter and Norell, Ulf},
61 title = {A Brief Overview of Agda --- A Functional Language with Dependent Types},
62 booktitle = {Proceedings of the 22Nd International Conference on Theorem Proving in Higher Order Logics},
63 series = {TPHOLs '09},
64 year = {2009},
65 isbn = {978-3-642-03358-2},
66 location = {Munich, Germany},
67 pages = {73--78},
68 numpages = {6},
69 url = {http://dx.doi.org/10.1007/978-3-642-03359-9_6},
70 doi = {10.1007/978-3-642-03359-9_6},
71 acmid = {1616085},
72 publisher = {Springer-Verlag},
73 address = {Berlin, Heidelberg},
74}
75
76@book{lof,
77 title = "Intuitionistic type theory",
78 author = "Martin-Löf, Per and Sambin, Giovanni",
79 series = "Studies in proof theory",
80 publisher = "Bibliopolis",
81 address = "Napoli",
82 url = "http://opac.inria.fr/record=b1093069",
83 isbn = "88-7088-105-9",
84 year = 1984
85}
86
87@book{nordstrom90,
88 address = {USA},
89 author = {Nordstr\"{o}m, Bengt and Petersson, Kent and Smith, Jan M.},
90 citeulike-linkout-0 = {http://www.cs.chalmers.se/Cs/Research/Logic/book/},
91 citeulike-linkout-1 = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20\&path=ASIN/0198538146},
92 citeulike-linkout-10 = {http://www.librarything.com/isbn/0198538146},
93 citeulike-linkout-2 = {http://www.amazon.de/exec/obidos/redirect?tag=citeulike01-21\&path=ASIN/0198538146},
94 citeulike-linkout-3 = {http://www.amazon.fr/exec/obidos/redirect?tag=citeulike06-21\&path=ASIN/0198538146},
95 citeulike-linkout-4 = {http://www.amazon.jp/exec/obidos/ASIN/0198538146},
96 citeulike-linkout-5 = {http://www.amazon.co.uk/exec/obidos/ASIN/0198538146/citeulike00-21},
97 citeulike-linkout-6 = {http://www.amazon.com/exec/obidos/redirect?tag=citeulike07-20\&path=ASIN/0198538146},
98 citeulike-linkout-7 = {http://www.worldcat.org/isbn/0198538146},
99 citeulike-linkout-8 = {http://books.google.com/books?vid=ISBN0198538146},
100 citeulike-linkout-9 = {http://www.amazon.com/gp/search?keywords=0198538146\&index=books\&linkCode=qs},
101 day = {19},
102 edition = {0},
103 howpublished = {Hardcover},
104 isbn = {0198538146},
105 keywords = {type-theory},
106 month = jul,
107 posted-at = {2008-08-07 16:37:39},
108 priority = {2},
109 publisher = {Oxford University Press},
110 title = {{Programming in Martin-L\"{o}f's Type Theory: An Introduction}},
111 url = {http://www.cs.chalmers.se/Cs/Research/Logic/book/},
112 year = {1990}
113}
114
115@book{Sorensen,
116 author = {S{\o}rensen, Morten Heine and Urzyczyn, Pawel},
117 title = {Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics)},
118 year = {2006},
119 isbn = {0444520775},
120 publisher = {Elsevier Science Inc.},
121 address = {New York, NY, USA},
122}
123
124@inproceedings{Guidi,
125 author = {Guidi, Claudio and Lucchi, Roberto and Gorrieri, Roberto and Busi, Nadia and Zavattaro, Gianluigi},
126 title = {SOCK: A Calculus for Service Oriented Computing},
127 booktitle = {Proceedings of the 4th International Conference on Service-Oriented Computing},
128 series = {ICSOC'06},
129 year = {2006},
130 isbn = {3-540-68147-7, 978-3-540-68147-2},
131 location = {Chicago, IL},
132 pages = {327--338},
133 numpages = {12},
134 url = {http://dx.doi.org/10.1007/11948148_27},
135 doi = {10.1007/11948148_27},
136 acmid = {2087316},
137 publisher = {Springer-Verlag},
138 address = {Berlin, Heidelberg},
139}
140
141@book{Milner1999,
142 author = {Milner, Robin},
143 title = {Communicating and Mobile Systems: The $\pi$-calculus},
144 year = {1999},
145 isbn = {0-521-65869-1},
146 publisher = {Cambridge University Press},
147 address = {New York, NY, USA},
148}
149@PHDTHESIS{Gui07,
150 title = {{Formalizing languages for Service Oriented Computing}},
151 author = {{Claudio} {Guidi}},
152 abstract = {Service Oriented Computing is a new programming paradigm for addressing
153 distributed system design issues. Services are autonomous computational entities
154 which can be dynamically discovered and composed in order to form more complex
155 systems able to achieve different kinds of task. E-government, e-business and
156 e-science are some examples of the IT areas where Service Oriented Computing
157 will be exploited in the next years. At present, the most credited Service
158 Oriented Computing technology is that of Web Services, whose specifications are
159 enriched day by day by industrial consortia without following a precise and
160 rigorous approach. This PhD thesis aims, on the one hand, at modelling Service
161 Oriented Computing in a formal way in order to precisely define the main
162 concepts it is based upon and, on the other hand, at defining a new approach,
163 called bipolar approach, for addressing system design issues by synergically
164 exploiting choreography and orchestration languages related by means of a
165 mathematical relation called conformance. Choreography allows us to describe
166 systems of services from a global view point whereas orchestration supplies a
167 means for addressing such an issue from
168 a local perspective. In this work we present SOCK, a process algebra
169 based language inspired by the Web Service orchestration language
170 WS-BPEL which catches the essentials of Service Oriented Computing. From the
171 definition of SOCK we will able to define a general model for dealing with
172 Service Oriented Computing where services and systems of services are related to
173 the design of finite state automata and process algebra concurrent systems,
174 respectively. Furthermore, we introduce a formal language for dealing with
175 choreography. Such a language is equipped with a formal semantics and it forms,
176 together with a subset of the SOCK calculus, the bipolar framework. Finally, we
177 present JOLIE which is a Java implentation of a subset of the SOCK calculus and
178 it is part of the bipolar framework we intend to promote.},
179 series = {UBLCS},
180 volume = {2007-07},
181 year = {2007},
182 url = {http://www.cs.unibo.it/pub/TR/UBLCS/2007/2007-07.pdf},
183 institution = {Computer Science Department - University
184of Bologna},
185 partner = {UNIBO},
186 status = {public},
187 task = {T2.1, T2.2, T2.3, T5.2},
188}
189
190@misc{BPEL,
191title = {{WS-BPEL} {OASIS} {W}eb {S}ervices {B}usiness {P}rocess {E}xecution {L}anguage. Accessed {April} 2016.},
192howpublished =
193{\url{http://docs.oasis-open.org/wsbpel/2.0/wsbpel-specification-draft.html}}
194}
195
196@Misc{jolierepo,
197 author = {Evgenii Akentev},
198 title = "{Verified type checker for Jolie programming language}",
199 note = {\url{https://github.com/welltyped/jolie}}
200}
201
202@article{Neis,
203 author = {Neis, Georg and Hur, Chung-Kil and Kaiser, Jan-Oliver and McLaughlin, Craig and Dreyer, Derek and Vafeiadis, Viktor},
204 title = {Pilsner: A Compositionally Verified Compiler for a Higher-order Imperative Language},
205 journal = {SIGPLAN Not.},
206 issue_date = {September 2015},
207 volume = {50},
208 number = {9},
209 month = aug,
210 year = {2015},
211 issn = {0362-1340},
212 pages = {166--178},
213 numpages = {13},
214 url = {http://doi.acm.org/10.1145/2858949.2784764},
215 doi = {10.1145/2858949.2784764},
216 acmid = {2784764},
217 publisher = {ACM},
218 address = {New York, NY, USA},
219 keywords = {Compositional compiler verification, abstract types, higher-order state, parametric simulations, recursive types, transitivity},
220}
221
222@article{Leroy,
223 author = {Leroy, Xavier},
224 title = {A Formally Verified Compiler Back-end},
225 journal = {J. Autom. Reason.},
226 issue_date = {December 2009},
227 volume = {43},
228 number = {4},
229 month = dec,
230 year = {2009},
231 issn = {0168-7433},
232 pages = {363--446},
233 numpages = {84},
234 url = {http://dx.doi.org/10.1007/s10817-009-9155-4},
235 doi = {10.1007/s10817-009-9155-4},
236 acmid = {1666216},
237 publisher = {Springer-Verlag New York, Inc.},
238 address = {Secaucus, NJ, USA},
239 keywords = {Compiler transformations and optimizations, Compiler verification, Formal methods, Program proof, Semantic preservation, The Coq theorem prover},
240}
241
242@Misc{agda,
243 author = {Chalmers University of Technology. Accessed April 2017.},
244 title = "{Agda}",
245 note = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}}
246}
247
248@incollection{MGZ14,
249 author = {Fabrizio Montesi and
250 Claudio Guidi and
251 Gianluigi Zavattaro},
252 title = {{Service-Oriented Programming with Jolie}},
253 booktitle = {Web Services Foundations},
254 publisher = {Springer},
255 pages = {81--107},
256 year = {2014}
257}
258
259@book{engelfriet,
260 title={Structural Congruence in the Pi-calculus with Potential Replication},
261 author={Engelfriet, J. and Gelsema, T. and Rijksuniversiteit te Leiden. LIACS Leiden Institute of Advanced Computer Science},
262 series={Technical report LIACS Leiden Institute of Advanced Computer Science},
263 url={https://books.google.ru/books?id=QZ1wnQEACAAJ},
264 year={2000},
265 publisher={Leiden University}
266}
267
268@inproceedings{zhao2012formalizing,
269 title={Formalizing the LLVM intermediate representation for verified program transformations},
270 author={Zhao, Jianzhou and Nagarakatte, Santosh and Martin, Milo MK and Zdancewic, Steve},
271 booktitle={ACM SIGPLAN Notices},
272 volume={47},
273 number={1},
274 pages={427--440},
275 year={2012},
276 organization={ACM}
277}
278
279@Misc{redprl,
280 author = {Jon Sterling},
281 title = {The {People}'s {Refinement} {Logic}},
282 note = {\url{http://www.redprl.org}}
283}
284
285@Misc{coq,
286 title={The Coq Proof Assistant},
287 author={Gérard Huet, Thierry Coquand},
288 note={\url{https://coq.inria.fr}}
289}
290
291@Misc{isabelle,
292 title={The Isabelle theorem prover},
293 author = {Lawrence Paulson},
294 note = {\url{http://isabelle.in.tum.de}}
295}
296
297
298@inproceedings{de2015lean,
299 title={The Lean theorem prover (system description)},
300 author={de Moura, Leonardo and Kong, Soonho and Avigad, Jeremy and Van Doorn, Floris and von Raumer, Jakob},
301 booktitle={International Conference on Automated Deduction},
302 pages={378--388},
303 year={2015},
304 organization={Springer}
305}
306
307@phdthesis{altenkirch1993constructions,
308 title={Constructions, inductive types and strong normalization},
309 author={Altenkirch, Thorsten},
310 school={Citeseer}
311}
312
313@incollection{crole1993deriving,
314 title={Deriving category theory from type theory},
315 author={Crole, Roy L},
316 booktitle={Theory and Formal Methods 1993},
317 pages={15--26},
318 year={1993},
319 publisher={Springer}
320}
321
322@article{coquand1988calculus,
323 title={The calculus of constructions},
324 author={Coquand, Thierry and Huet, G{\'e}rard},
325 journal={Information and computation},
326 volume={76},
327 number={2-3},
328 pages={95--120},
329 year={1988},
330 publisher={Elsevier}
331}
332
333@misc{hottwebsite,
334 title={Homotopy {Type} {Theory}},
335 note={\url{http://homotopytypetheory.org}}
336 }
337
338@article{voevodsky2006very,
339 title={A very short note on the homotopy $\lambda$-calculus},
340 author={Voevodsky, Vladimir},
341 year={2006}
342}
343
344@inproceedings{pfenning1990inductively,
345 title={Inductively defined types in the Calculus of Constructions},
346 author={Pfenning, Frank and Paulin-Mohring, Christine},
347 booktitle={Mathematical Foundations of Programming Semantics},
348 pages={209--228},
349 year={1990},
350 organization={Springer}
351}
352
353@inproceedings{constable2011trimuph,
354 title={The trimuph of types: Creating a logic of computational reality},
355 author={Constable, Robert L}
356}
357
358@book{constable1986implementing,
359 title={Implementing mathematics},
360 author={Constable, RL and Allen, SF and Bromley, HM and Cleaveland, WR and Cremer, JF and Harper, RW and Howe, DJ and Knoblock, TB and Mendler, NP and Panangaden, P and others}
361}
362
363@incollection{constable2002naive,
364 title={Naive computational type theory},
365 author={Constable, Robert L},
366 booktitle={Proof and System-Reliability},
367 pages={213--259},
368 year={2002},
369 publisher={Springer}
370}
371
372@article{gordon1979edinburgh,
373 title={Edinburgh lcf},
374 author={Gordon, Michael},
375 journal={A Mechanized Logic of Computation},
376 year={1979},
377 publisher={Springer-Verlag}
378}
379
380@article{cohen2016cubical,
381 title={Cubical type theory: a constructive interpretation of the univalence axiom},
382 author={Cohen, Cyril and Coquand, Thierry and Huber, Simon and M{\"o}rtberg, Anders},
383 journal={arXiv preprint arXiv:1611.02108},
384 year={2016}
385}
386
387@book{milner1997definition,
388 title={The definition of standard ML: revised},
389 author={Milner, Robin},
390 year={1997}
391}
392
393@online{literateagda,
394 title={Literate Agda},
395 howpublished={\url{http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.LiterateAgda}}
396}