source: Deliverables/D4.1/ITP-Paper/itp-2011.bib @ 815

Last change on this file since 815 was 815, checked in by mulligan, 9 years ago

some changes

File size: 6.4 KB
Line 
1@article
2{ asperti:user:2007,
3  author = {Andrea Asperti and Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli},
4  title = {User interaction with the {Matita} proof assistant},
5  journal = {Journal of Automated Reasoning},
6  pages = {109--139},
7  volume = {39},
8  issue = {2},
9  year = {2007}
10}
11
12@article
13{ bate:wcet:2011,
14  author = {Iain Bate and Usman Khan},
15  title = {{WCET} analysis of modern processors using multi-criteria optimisation},
16  journal = {Empirical Software Engineering},
17  pages = {5--28},
18  volume = {16},
19  issue = {1},
20  year = {2011}
21}
22
23@article
24{ leroy:formal:2009,
25  author = {Xavier Leroy},
26  title = {Formal verification of a realistic compiler},
27  journal = {Communications of the {Association of Computing Machinery}},
28  volume = {52},
29  number = {7},
30  pages = {107--115},
31  year = {2009}
32}
33
34@article
35{ leroy:formally:2009,
36  author = {Xavier Leroy},
37  title = {A formally verified compiler back-end},
38  journal = {Journal of Automated Reasoning},
39  volume = {43},
40  number = {4},
41  pages = {363--446},
42  year = {2009}
43}
44
45@article
46{ luo:coercive:1999,
47  author = {Zhaohui Luo},
48  title = {Coercive subtyping},
49  journal = {Journal of Logic and Computation},
50  volume = {9},
51  number = {1},
52  pages = {105--130},
53  year = {1999}
54}
55
56@inproceedings
57{ yan:wcet:2008,
58  author = {Jun Yan and Wei Zhang},
59  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
60  booktitle = {Proceedings of the $\mathrm{14^{th}}$ {IEEE} Symposium on Real-time and Embedded Technology and Applications},
61  pages = {80--89},
62  year = {2008}
63}
64
65@inproceedings
66{ atkey:coqjvm:2007,
67  author = {Robert Atkey},
68  title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
69  booktitle = {Proceedings of the Conference of the {TYPES} Project},
70  pages = {18--32},
71  year = {2007}
72}
73
74@inproceedings
75{ blanqui:designing:2010,
76  title = {Designing a {CPU} model: from a pseudo-formal document to fast code},
77  author = {Fr\'ed\'eric Blanqui and Claude Helmstetter and Vania Joloboff and Jean-Fran\c{c}ois Monin and Xiaomu Shi},
78  booktitle = {Proceedings of the $\mathrm{3^{rd}}$ Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools},
79  year = {2010}
80}
81
82@inproceedings
83{ blazy:formal:2006,
84  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
85  title = {Formal Verification of a {C} Compiler Front-End},
86  booktitle = {Proceedings of the International Symposium on Formal Methods},
87  pages = {460--475},
88  year = {2006}
89}
90
91@inproceedings
92{ chlipala:verified:2010,
93  author = {Adam Chlipala},
94  title = {A verified compiler for an impure functional language},
95  booktitle = {Proceedings of the $\mathrm{37^{th}}$ Annual Symposium on Principles of Programming Languages},
96  pages = {93--106},
97  year = {2010}
98}
99
100@inproceedings
101{ fox:trustworthy:2010,
102  author = {Anthony Fox and Magnus O. Myreen},
103  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
104  booktitle = {Proceedings of the $\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving},
105  pages = {243--258},
106  year = {2010}
107}
108
109@inproceedings
110{ garrigue:programming:1998,
111  author = {Jacques Garrigue},
112  title = {Programming with polymorphic variants},
113  booktitle = {{ML} Workshop},
114  year = {1998}
115}
116
117@inproceedings
118{ leijen:domain:1999,
119  author = {Daan Leijen and Erik Meijer},
120  title = {Domain specific embedded compilers},
121  booktitle = {Proceedings of the $\mathrm{2^{nd}}$ Conference on Domain Specific Languages},
122  pages = {109--122},
123  year = {1999}
124}
125
126@inproceedings
127{ sarkar:semantics:2009,
128  author = {Susmit Sarkar and Peter Sewell and Francesco Zappa Nardelli and Scott Owens and Tom Ridge and Thomas Braibant and Magnus O. Myreen and Jade Alglave},
129  title = {The semantics of {x86-CC} multiprocessor machine code},
130  booktitle = {Proceedings of the $\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},
131  pages = {379--391},
132  year = {2009}
133}
134
135@inproceedings
136{ shankar:principles:1999,
137  author = {Natarajan Shankar and Sam Owre},
138  title = {Principles and Pragmatics of Subtyping in {PVS}},
139  booktitle = {Recent Trends in Algebraic Development Techniques},
140  pages = {37--52},
141  year = {1999}
142}
143
144@inproceedings
145{ sozeau:subset:2006,
146  author = {Matthieu Sozeau},
147  title = {Subset coercions in {Coq}},
148  booktitle = {Proceedings of the Conference of the {TYPES} Project},
149  pages = {237--252},
150  year = {2006}
151}
152
153@inproceedings
154{ xi:guarded:2003,
155  author = {Hongwei Xi and Chiyan Chen and Gang Chen},
156  title = {Guarded recursive datatype constructors},
157  booktitle = {Proceedings of the $\mathrm{30^{th}}$ Annual Symposium on Principles of Programming Languages},
158  pages = {224--235},
159  year = {2003}
160}
161
162@misc
163{ cerco:2011,
164  title = {The {CerCo} {FET-Open} Project},
165  howpublished = {\url{http://cerco.cs.unibo.it}},
166  year = {2011},
167  key = {{CerCo}}
168}
169
170@misc
171{ cerco-code:2011,
172  title = {{CerCo Deliverable D4.1}: Matita and O'Caml code},
173  howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1_Code.tar.gz}},
174  year = {2011},
175  key = {{CerCo-code}}
176}
177
178@misc
179{ cerco-report:2011,
180  title = {{CerCo Deliverable D4.1}:: executable formal semantics of machine code},
181  howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1.pdf}},
182  year = {2011},
183  key = {{CerCo-report}}
184}
185
186@misc
187{ mcu8051ide:2010,
188  title = {{MCU 8051 IDE} 1.3.11},
189  howpublished = {\url{http://mcu8051ide.sourceforge.net/}},
190  year = {2010},
191  key = {{MCU}}
192}
193
194@misc
195{ oliboni:matita:2008,
196  author = {Cosimo A. Oliboni},
197  title = {{Matita} come Supporto per Specifiche Eseguibili: Formalizzazione Interattiva dei Microcontroller a 8 bit {Freescale}},
198  institution = {Dipartimento di Scienze dell'Informazione, Universit\`a di Bologna},
199  howpublished = {\url{http://matita.cs.unibo.it/library.shtml}},
200  year = {2008}
201}
202
203@misc
204{ sdcc:2010,
205  title = {Small Device {C} Compiler {(SDCC)} 3.0.0},
206  howpublished = {\url{http://sdcc.sourceforge.net/}},
207  year = {2010},
208  key = {{SDCC}}
209}
210
211@misc
212{ siemens:2011,
213  title = {{Siemens Semiconductor Group} 8051 derivative instruction set},
214  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
215  year = {2011},
216  key = {{Siemens}}
217}
218
219@techreport
220{ amadio:certifying:2010,
221  author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
222  title = {Cerifying cost annotations in compilers},
223  institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
224  year = {2010}
225}
Note: See TracBrowser for help on using the repository browser.