source: Papers/itp-2013/ccexec.bib @ 3329

Last change on this file since 3329 was 2635, checked in by sacerdot, 6 years ago

...

File size: 25.1 KB
Line 
1Entry made up
2
3@article{MilnerWeyhrauch72,
4  title = {Proving compiler correctness in a mechanized logic},
5  author = {R. Milner and R. Weyhrauch},
6  journal = {Machine Intelligence},
7  year = 1972,
8  volume = 7,
9  pages = {51--70},
10  editors = {Bernard Meltzer and Donald Michie},
11  publisher = {Edinburgh University Press}
12}
13
14Entry from ACM Digital Library.
15
16@inproceedings{Tatlock:2010:BEV:1806596.1806611,
17 author = {Tatlock, Zachary and Lerner, Sorin},
18 title = {Bringing extensibility to verified compilers},
19 booktitle = {Proceedings of the 2010 ACM SIGPLAN conference on Programming language design and implementation},
20 series = {PLDI '10},
21 year = {2010},
22 isbn = {978-1-4503-0019-3},
23 location = {Toronto, Ontario, Canada},
24 pages = {111--121},
25 numpages = {11},
26 url = {http://doi.acm.org/10.1145/1806596.1806611},
27 doi = {http://doi.acm.org/10.1145/1806596.1806611},
28 acmid = {1806611},
29 publisher = {ACM},
30 address = {New York, NY, USA},
31 keywords = {compiler optimization, correctness, extensibility},
32}
33
34Entry from ACM Digitial Library.  (With name fixup)
35
36@inproceedings{Sevcik:2011:RCV:1926385.1926393,
37 author = {\v{S}ev\v{c}\'{i}k, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
38 title = {Relaxed-memory concurrency and verified compilation},
39 booktitle = {Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
40 series = {POPL '11},
41 year = {2011},
42 isbn = {978-1-4503-0490-0},
43 location = {Austin, Texas, USA},
44 pages = {43--54},
45 numpages = {12},
46 url = {http://doi.acm.org/10.1145/1926385.1926393},
47 doi = {http://doi.acm.org/10.1145/1926385.1926393},
48 acmid = {1926393},
49 publisher = {ACM},
50 address = {New York, NY, USA},
51 keywords = {relaxed memory models, semantics, verifying compilation},
52}
53
54Entry from ACM Digital Library.
55
56@article{Leroy:2009:FVR:1538788.1538814,
57 author = {Leroy, Xavier},
58 title = {Formal verification of a realistic compiler},
59 journal = {Commun. ACM},
60 issue_date = {July 2009},
61 volume = {52},
62 issue = {7},
63 month = jul,
64 year = {2009},
65 issn = {0001-0782},
66 pages = {107--115},
67 numpages = {9},
68 url = {http://doi.acm.org/10.1145/1538788.1538814},
69 doi = {http://doi.acm.org/10.1145/1538788.1538814},
70 acmid = {1538814},
71 publisher = {ACM},
72 address = {New York, NY, USA},
73}
74
75Entry from ACM Digital Library.
76
77@inproceedings{1328444,
78 author = {Jean-Baptiste Tristan and Xavier Leroy},
79 title = {Formal verification of translation validators: a case study on instruction scheduling optimizations},
80 booktitle = {POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
81 year = {2008},
82 isbn = {978-1-59593-689-9},
83 pages = {17--27},
84 location = {San Francisco, California, USA},
85 doi = {http://doi.acm.org/10.1145/1328438.1328444},
86 publisher = {ACM},
87 address = {New York, NY, USA},
88 }
89
90Entry made up.
91
92@inproceedings{coqextr02,
93  title  = {A New Extraction for {C}oq},
94  author = {Pierre Letouzey},
95  booktitle = {Types for Proofs and Programs (TYPES 2002)},
96  year   = 2003,
97  volume = 2646,
98  series = {Lecture Notes in Computer Science},
99  pages  = {200--219},
100  publisher = {Springer-Verlag},
101  doi    = {10.1007/3-540-39185-1_12}
102}
103
104Entry from Springerlink with obvious corrections.
105
106@article {springerlink:10.1007/s10817-009-9148-3,
107   author = {Blazy, Sandrine and Leroy, Xavier},
108   affiliation = {ENSIIE 1 square de la Résistance 91025 Evry cedex France},
109   title = {Mechanized Semantics for the {Clight} Subset of the {C} Language},
110   journal = {Journal of Automated Reasoning},
111   publisher = {Springer Netherlands},
112   issn = {0168-7433},
113   keyword = {Computer Science},
114   pages = {263-288},
115   volume = {43},
116   issue = {3},
117   url = {http://dx.doi.org/10.1007/s10817-009-9148-3},
118   doi = {10.1007/s10817-009-9148-3},
119   abstract = {This article presents the formal semantics of a large subset of the C language called Clight. Clight includes pointer arithmetic, struct and union types, C loops and structured switch statements. Clight is the source language of the CompCert verified compiler. The formal semantics of Clight is a big-step operational semantics that observes both terminating and diverging executions and produces traces of input/output events. The formal semantics of Clight is mechanized using the Coq proof assistant. In addition to the semantics of Clight, this article describes its integration in the CompCert verified compiler and several ways by which the semantics was validated.},
120   year = {2009}
121}
122
123Entry made up
124
125@manual{coq83,
126  title = {The {Coq} Proof Assistant: Reference Manual, Version 8.3},
127  author = {The Coq Development Team},
128  organization = {INRIA},
129  year = 2010,
130  url = {http://coq.inria.fr/distrib/8.3pl2/refman/}
131}
132
133Entry made up
134
135@techreport{c99,
136  title = {Programming languages --- {C}},
137  key = {C99},
138  institution = {ISO},
139  year = {1999},
140  type = {International standard},
141  number = {ISO/IEC 9899:1999}
142}
143
144Entry made up.
145
146@article{compcert1,
147  author = {Xavier Leroy},
148  title = {Formal verification of a realistic compiler},
149  journal = {Communications of the ACM},
150  year = 2009,
151  volume = 52,
152  number = 7,
153  pages = {107--115},
154  url = {http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf},
155  urlpublisher = {http://doi.acm.org/10.1145/1538788.1538814},
156  hal = {http://hal.archives-ouvertes.fr/inria-00415861/},
157  pubkind = {journal-int-mono},
158  abstract = {This paper reports on the development and formal verification (proof
159of semantic preservation) of CompCert, a compiler from Clight (a
160large subset of the C programming language) to PowerPC assembly code,
161using the Coq proof assistant both for programming the compiler and
162for proving its correctness.  Such a verified compiler is useful in
163the context of critical software and its formal verification: the
164verification of the compiler guarantees that the safety properties
165proved on the source code hold for the executable compiled code as
166well.}
167}
168
169@article{compcert2,
170  title = {Formal Verification of a {C}-like Memory Model and Its Uses for Verifying Program Transformations},
171  author = {Xavier Leroy and Sandrine Blazy},
172  journal = {Journal of Automated Reasoning},
173  year = 2008,
174  volume = 41,
175  number = 1,
176  pages = {1--31},
177  doi = {10.1007/s10817-008-9099-0}
178}
179
180@article{compcert3,
181  author = {Xavier Leroy},
182  title = {A formally verified compiler back-end},
183  journal = {Journal of Automated Reasoning},
184  volume = 43,
185  number = 4,
186  pages = {363--446},
187  year = 2009,
188  url = {http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf},
189  urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9155-4},
190  hal = {http://hal.inria.fr/inria-00360768/},
191  pubkind = {journal-int-mono}
192}
193
194
195Entry from ACM Digital Library with obvious correction.
196
197@inproceedings{Yang:2011:FUB:1993498.1993532,
198 author = {Yang, Xuejun and Chen, Yang and Eide, Eric and Regehr, John},
199 title = {Finding and understanding bugs in {C} compilers},
200 booktitle = {Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation},
201 series = {PLDI '11},
202 year = {2011},
203 isbn = {978-1-4503-0663-8},
204 location = {San Jose, California, USA},
205 pages = {283--294},
206 numpages = {12},
207 url = {http://doi.acm.org/10.1145/1993498.1993532},
208 doi = {http://doi.acm.org/10.1145/1993498.1993532},
209 acmid = {1993532},
210 publisher = {ACM},
211 address = {New York, NY, USA},
212 keywords = {automated testing, compiler defect, compiler testing, random program generation, random testing},
213}
214
215Entry made up.
216
217@inproceedings{cil02,
218  title  = {{CIL}: Intermediate Language and Tools for Analysis and Transformation of {C} Programs},
219  author = {George C. Necula and Scott McPeak and Shree P. Rahul and Westley Weimer},
220  booktitle = {Compiler Construction: 11th International Conference (CC 2002)},
221  pages = {213--228},
222  year   = 2002,
223  editor = {R. Nigel Horspool},
224  volume = 2304,
225  series = {Lecture Notes in Computer Science},
226  publisher = {Springer},
227  doi = {10.1007/3-540-45937-5_16}
228}
229
230Entry made up.
231
232@manual{gccint4.4,
233  title = {{GNU} {Compiler} {Collection} {(GCC)} Internals},
234  note = {Version 4.4.3},
235  organization = {Free Software Foundation},
236  year = 2008
237}
238
239Entry from ACM Digital Library with corrected accent, capital.
240
241@inproceedings{Ellison:2012:EFS:2103656.2103719,
242 author = {Ellison, Chucky and Ro{\c s}u, Grigore},
243 title = {An executable formal semantics of {C} with applications},
244 booktitle = {Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
245 series = {POPL '12},
246 year = {2012},
247 isbn = {978-1-4503-1083-3},
248 location = {Philadelphia, PA, USA},
249 pages = {533--544},
250 numpages = {12},
251 url = {http://doi.acm.org/10.1145/2103656.2103719},
252 doi = {10.1145/2103656.2103719},
253 acmid = {2103719},
254 publisher = {ACM},
255 address = {New York, NY, USA},
256 keywords = {C, k, semantics},
257} 
258
259Entry from Springerlink. Note -> DOI.
260
261@Inproceedings{clockfunctions,
262  author    = "S. Ray and J S. Moore",
263  title     = "{Proof Styles in Operational Semantics}",
264  editor    = "A. J. Hu and A. K. Martin",
265  booktitle = "{Proceedings of the $5$th International Conference on
266                Formal Methods in Computer-Aided Design (FMCAD 2004)}",
267  series    = "{LNCS}",
268  volume    = "3312",
269  address   = "{Austin, TX}",
270  publisher = "{Springer}",
271  month     = nov,
272  pages     = "67-81",
273  year      = 2004
274}
275
276@article {piton,
277   author = {Moore, J Strother},
278   title = {A mechanically verified language implementation},
279   journal = {Journal of Automated Reasoning},
280   publisher = {Springer Netherlands},
281   issn = {0168-7433},
282   keyword = {Computer Science},
283   pages = {461-492},
284   volume = {5},
285   issue = {4},
286   url = {http://dx.doi.org/10.1007/BF00243133},
287   doi = {10.1007/BF00243133},
288   abstract = {This paper briefly describes a programming language, its implementation on a microprocessor via a compiler and link-assembler, and the mechanically checked proof of the correctness of the implementation. The programming language, called Piton, is a high-level assembly language designed for verified applications and as the target language for high-level language compilers. It provides executeonly programs, recursive subroutine call and return, stack based parameter passing, local variables, global variables and arrays, a user-visible stack for intermediate results, and seven abstract data types including integers, data addresses, program addresses and subroutine names. Piton is formally specified by an interpreter written for it in the computational logic of Boyer and Moore. Piton has been implemented on the FM8502, a general purpose microprocessor whose gate-level design has been mechanically proved to implement its machine code interpreter. The FM8502 implementation of Piton is via a function in the Boyer-Moore logic which maps a Piton initial state into an FM8502 binary core image. The compiler and link-assembler are both defined as functions in the logic. The implementation requires approximately 36K bytes and 1400 lines of prettyprinted source code in the Pure Lisp-like syntax of the logic. The implementation has been mechanically proved correct. In particular, if a Piton state can be run to completion without error, then the final values of all the global data structures can be ascertained from an inspection of an FM8502 core image obtained by running the core image produced by the compiler and link-assembler. Thus, verified Piton programs running on FM8502 can be thought of as having been verified down to the gate level.},
289   year = {1989}
290}
291
292Entry from Springerlink, plus accent fix and doi changed to doi rather than
293note. And capital.
294
295@incollection {springerlink:10.1007/978-3-642-22863-6_17,
296   author = {Lochbihler, Andreas and Bulwahn, Lukas},
297   affiliation = {Karlsruher Institut f{\"{u}}r Technologie, Germany},
298   title = {Animating the Formalised Semantics of a {J}ava-Like Language},
299   booktitle = {Interactive Theorem Proving},
300   series = {Lecture Notes in Computer Science},
301   editor = {van Eekelen, Marko and Geuvers, Herman and Schmaltz, Julien and Wiedijk, Freek},
302   publisher = {Springer Berlin / Heidelberg},
303   isbn = {978-3-642-22862-9},
304   keyword = {Computer Science},
305   pages = {216-232},
306   volume = {6898},
307   url = {http://dx.doi.org/10.1007/978-3-642-22863-6_17},
308   doi = {10.1007/978-3-642-22863-6_17},
309   abstract = {Considerable effort has gone into the techniques of extracting executable code from formal specifications and animating them. We show how to apply these techniques to the large JinjaThreads formalisation. It models a substantial subset of multithreaded Java source and bytecode in Isabelle/HOL and focuses on proofs and modularity whereas code generation was of little concern in its design. Employing Isabelle’s code generation facilities, we obtain a verified Java interpreter that is sufficiently efficient for running small Java programs. To this end, we present refined implementations for common notions such as the reflexive transitive closure and Russell’s definite description operator. From our experience, we distill simple guidelines on how to develop future formalisations with executability in mind.},
310   year = {2011}
311}
312
313Entry from ACM Digital Library (I've only searched it for testing, not read it).
314
315@article{Klein:2006:MMJ:1146809.1146811,
316 author = {Klein, Gerwin and Nipkow, Tobias},
317 title = {A machine-checked model for a {Java}-like language, virtual machine, and compiler},
318 journal = {ACM Trans. Program. Lang. Syst.},
319 issue_date = {July 2006},
320 volume = {28},
321 number = {4},
322 month = jul,
323 year = {2006},
324 issn = {0164-0925},
325 pages = {619--695},
326 numpages = {77},
327 url = {http://doi.acm.org/10.1145/1146809.1146811},
328 doi = {10.1145/1146809.1146811},
329 acmid = {1146811},
330 publisher = {ACM},
331 address = {New York, NY, USA},
332 keywords = {Java, operational semantics, theorem proving},
333} 
334
335Entry from sciencedirect. Remove dodgy number and note.
336
337@article{Leinenbach200823,
338title = "Pervasive Compiler Verification – From Verified Programs to Verified Systems",
339journal = "Electronic Notes in Theoretical Computer Science",
340volume = "217",
341pages = "23 - 40",
342year = "2008",
343issn = "1571-0661",
344doi = "10.1016/j.entcs.2008.06.040",
345url = "http://www.sciencedirect.com/science/article/pii/S1571066108003836",
346author = "Dirk Leinenbach and Elena Petrova",
347keywords = "Compiler Verification",
348keywords = "Theorem Proving",
349keywords = "System Verification",
350keywords = "HOL",
351keywords = "Hoare Logic",
352abstract = "We report in this paper on the formal verification of a simple compiler for the C-like programming language C0. The compiler correctness proof meets the special requirements of pervasive system verification and allows to transfer correctness properties from the C0 layer to the assembler and hardware layers. The compiler verification is split into two parts: the correctness of the compiling specification (which can be translated to executable ML code via Isabelle's code generator) and the correctness of a C0 implementation of this specification. We also sketch a method to solve the boot strap problem, i.e., how to obtain a trustworthy binary of the C0 compiler from its C0 implementation. Ultimately, this allows to prove pervasively the correctness of compiled C0 programs in the real system."
353}
354
355@book{while,
356 author = {Nielson, Flemming and Nielson, Hanne R. and Hankin, Chris},
357 title = {Principles of Program Analysis},
358 year = {1999},
359 isbn = {3540654100},
360 publisher = {Springer-Verlag New York, Inc.},
361 address = {Secaucus, NJ, USA},
362}
363
364@incollection{easylabelling,
365year={2012},
366isbn={978-3-642-32468-0},
367booktitle={Formal Methods for Industrial Critical Systems},
368volume={7437},
369series={Lecture Notes in Computer Science},
370editor={Stoelinga, Mariëlle and Pinger, Ralf},
371doi={10.1007/978-3-642-32469-7_3},
372title={Certifying and Reasoning on Cost Annotations in {C} Programs},
373url={http://dx.doi.org/10.1007/978-3-642-32469-7_3},
374publisher={Springer Berlin Heidelberg},
375author={Ayache, Nicolas and Amadio, RobertoM. and R\'egis-Gianas, Yann},
376pages={32-46}
377}
378
379@incollection{functionallabelling,
380year={2012},
381isbn={978-3-642-32494-9},
382booktitle={Foundational and Practical Aspects of Resource Analysis},
383volume={7177},
384series={Lecture Notes in Computer Science},
385editor={Peña, Ricardo and Eekelen, Marko and Shkaravska, Olha},
386doi={10.1007/978-3-642-32495-6_5},
387title={Certifying and Reasoning on Cost Annotations of Functional Programs},
388url={http://dx.doi.org/10.1007/978-3-642-32495-6_5},
389publisher={Springer Berlin Heidelberg},
390author={Amadio, RobertoM. and R\'egis-Gianas, Yann},
391pages={72-89},
392note={Extended version to appear in Higher Order and Symbolic Computation, 2013}
393}
394
395@inproceedings{framaC,
396 author = {Cuoq, Pascal and Kirchner, Florent and Kosmatov, Nikolai and Prevosto, Virgile and Signoles, Julien and Yakobowski, Boris},
397 title = {Frama-C: a software analysis perspective},
398 booktitle = {Proceedings of the 10th international conference on Software Engineering and Formal Methods},
399 series = {SEFM'12},
400 year = {2012},
401 isbn = {978-3-642-33825-0},
402 location = {Thessaloniki, Greece},
403 pages = {233--247},
404 numpages = {15},
405 url = {http://dx.doi.org/10.1007/978-3-642-33826-7_16},
406 doi = {10.1007/978-3-642-33826-7_16},
407 acmid = {2404250},
408 publisher = {Springer-Verlag},
409 address = {Berlin, Heidelberg},
410} 
411
412@article{cerco,
413  INIauthor    = {R. Amadio and A. Asperti and N. Ayache and
414                  B. Campbell and D. Mulligan and R. Pollack and
415                  Y. R{\'e}gis-Gianas and C. {Sacerdoti Coen} and I.
416                  Stark},
417  author    = {Roberto Amadio and Andrea Asperti and Nicholas Ayache and
418                  Brian Campbell and Dominic Mulligan and Randy Pollack and
419                  Yann R{\'e}gis-Gianas and Claudio {Sacerdoti Coen} and Ian
420                  Stark},
421  title     = {Certified Complexity},
422  journal   = {Procedia Computer Science},
423  volume    = 7,
424  year      = 2011,
425  pages     = {175--177},
426  doi       = {10.1016/j.procs.2011.09.054}
427}
428
429Entry from springerlink with accent corrections.
430
431@incollection {springerlink:10.1007/978-3-642-11970-5_13,
432   author = {Rideau, Silvain and Leroy, Xavier},
433   affiliation = {{\'{E}}cole Normale Sup{\'{e}}rieure 45 rue d’Ulm 75005 Paris France},
434   title = {Validating Register Allocation and Spilling},
435   booktitle = {Compiler Construction},
436   series = {Lecture Notes in Computer Science},
437   editor = {Gupta, Rajiv},
438   publisher = {Springer Berlin / Heidelberg},
439   isbn = {978-3-642-11969-9},
440   keyword = {Computer Science},
441   pages = {224-243},
442   volume = {6011},
443   url = {http://dx.doi.org/10.1007/978-3-642-11970-5_13},
444   doi = {10.1007/978-3-642-11970-5_13},
445   abstract = {Following the translation validation approach to high-assurance compilation, we describe a new algorithm for validating a posteriori the results of a run of register allocation. The algorithm is based on backward dataflow inference of equations between variables, registers and stack locations, and can cope with sophisticated forms of spilling and live range splitting, as well as many architectural irregularities such as overlapping registers. The soundness of the algorithm was mechanically proved using the Coq proof assistant.},
446   year = {2010}
447}
448
449Entry from springerlink with accent and title corrections.
450
451@incollection {springerlink:10.1007/978-3-642-28869-2_20,
452   author = {Jourdan, Jacques-Henri and Pottier, Fran{\c{c}}ois and Leroy, Xavier},
453   affiliation = {{\'{E}}cole Normale Sup{\'{e}}rieure, France},
454   title = {Validating {LR(1)} Parsers},
455   booktitle = {Programming Languages and Systems},
456   series = {Lecture Notes in Computer Science},
457   editor = {Seidl, Helmut},
458   publisher = {Springer Berlin / Heidelberg},
459   isbn = {978-3-642-28868-5},
460   keyword = {Computer Science},
461   pages = {397-416},
462   volume = {7211},
463   url = {http://dx.doi.org/10.1007/978-3-642-28869-2_20},
464   doi = {10.1007/978-3-642-28869-2_20},
465   abstract = {An LR (1) parser is a finite-state automaton, equipped with a stack, which uses a combination of its current state and one lookahead symbol in order to determine which action to perform next. We present a validator which, when applied to a context-free grammar and an automaton , checks that and agree. Validating the parser provides the correctness guarantees required by verified compilers and other high-assurance software that involves parsing. The validation process is independent of which technique was used to construct . The validator is implemented and proved correct using the Coq proof assistant. As an application, we build a formally-verified parser for the C99 language.},
466   year = {2012}
467}
468
469
470@techreport{EDI-INF-RR-1412,
471  author = {Brian Campbell and Randy Pollack},
472  title = {Executable Formal Semantics of {C}},
473  institution = {School of Informatics, University of Edinburgh},
474  year = 2010,
475  number = {EDI-INF-RR-1412}
476}
477
478Entry from springerlink, with obvious capitalisation correction and note -> doi.
479
480@incollection {springerlink:10.1007/3-540-49519-3_22,
481   author = {Strother Moore, J.},
482   affiliation = {The University of Texas at Austin Department of Computer Sciences Austin TX 78712-1188},
483   title = {Symbolic Simulation: An {ACL2} Approach},
484   booktitle = {Formal Methods in Computer-Aided Design},
485   series = {Lecture Notes in Computer Science},
486   editor = {Gopalakrishnan, Ganesh and Windley, Phillip},
487   publisher = {Springer Berlin / Heidelberg},
488   isbn = {978-3-540-65191-8},
489   keyword = {Computer Science},
490   pages = {530-530},
491   volume = {1522},
492   url = {http://dx.doi.org/10.1007/3-540-49519-3_22},
493   doi = {10.1007/3-540-49519-3_22},
494   abstract = {Executable formal specification can allow engineers to test (or simulate ) the specified system on concrete data before the system is implemented. This is beginning to gain acceptance and is just the formal analogue of the standard practice of building simulators in conventional programming languages such as C. A largely unexplored but potentially very useful next step is symbolic simulation , the “execution” of the formal specification on indeterminant data. With the right interface, this need not require much additional training of the engineers using the tool. It allows many tests to be collapsed into one. Furthermore, it familiarizes the working engineer with the abstractions and notation used in the design, thus allowing team members to speak clearly to one another. We illustrate these ideas with a formal specification of a simple computing machine in ACL2. We sketch some requirements on the interface, which we call a symbolic spreadsheet .},
495   year = {1998}
496}
497
498
499Entry from springerlink. Note -> doi.
500
501@incollection {springerlink:10.1007/978-3-642-03359-9_11,
502   author = {Berghofer, Stefan and Bulwahn, Lukas and Haftmann, Florian},
503   affiliation = {Technische Universitüt München Institut für Informatik Boltzmannstraße 3 85748 Garching Germany},
504   title = {Turning Inductive into Equational Specifications},
505   booktitle = {Theorem Proving in Higher Order Logics},
506   series = {Lecture Notes in Computer Science},
507   editor = {Berghofer, Stefan and Nipkow, Tobias and Urban, Christian and Wenzel, Makarius},
508   publisher = {Springer Berlin / Heidelberg},
509   isbn = {978-3-642-03358-2},
510   keyword = {Computer Science},
511   pages = {131-146},
512   volume = {5674},
513   url = {http://dx.doi.org/10.1007/978-3-642-03359-9_11},
514   doi = {10.1007/978-3-642-03359-9_11},
515   abstract = {Inductively defined predicates are frequently used in formal specifications. Using the theorem prover Isabelle , we describe an approach to turn a class of systems of inductively defined predicates into a system of equations using data flow analysis; the translation is carried out inside the logic and resulting equations can be turned into functional program code in SML , OCaml or Haskell using the existing code generator of Isabelle . Thus we extend the scope of code generation in Isabelle from functional to functional-logic programs while leaving the trusted foundations of code generation itself intact.},
516   year = {2009}
517}
518
519@Unpublished{loopoptimizations,
520 author = {Paolo Tranquilli},
521 title = {Indexed Labels for Loop Iteration Dependent Costs},
522 note = {to appear in Electronic Proceedings in Theoretical Computer Science, proceedings of Quantitative Aspects of
523Programming Languages and Systems (QAPL 2013)},
524 month = jan,
525 year = {2013},
526 url = {http://www.cs.unibo.it/~tranquil/content/docs/indlabels.pdf}
527}
528
529@incollection{matita1,
530year={2011},
531isbn={978-3-642-22437-9},
532booktitle={Automated Deduction – CADE-23},
533volume={6803},
534series={Lecture Notes in Computer Science},
535editor={Bjørner, Nikolaj and Sofronie-Stokkermans, Viorica},
536doi={10.1007/978-3-642-22438-6_7},
537title={The Matita Interactive Theorem Prover},
538url={http://dx.doi.org/10.1007/978-3-642-22438-6_7},
539publisher={Springer Berlin Heidelberg},
540author={Asperti, Andrea and Ricciotti, Wilmer and Sacerdoti Coen, Claudio and Tassi, Enrico},
541pages={64-69}
542}
543
544@article{matita2,
545year={2007},
546issn={0168-7433},
547journal={Journal of Automated Reasoning},
548volume={39},
549issue={2},
550doi={10.1007/s10817-007-9070-5},
551title={User Interaction with the Matita Proof Assistant},
552url={http://dx.doi.org/10.1007/s10817-007-9070-5},
553publisher={Springer Netherlands},
554keywords={Proof assistant; Interactive theorem proving; Digital libraries; XML; Mathematical knowledge management; Authoring},
555author={Asperti, Andrea and Sacerdoti Coen, Claudio and Tassi, Enrico and Zacchiroli, Stefano},
556pages={109-139},
557language={English}
558}
Note: See TracBrowser for help on using the repository browser.