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

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

changes with claudio

File size: 6.1 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{ blazy:formal:2006,
76  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
77  title = {Formal Verification of a {C} Compiler Front-End},
78  booktitle = {Proceedings of the International Symposium on Formal Methods},
79  pages = {460--475},
80  year = {2006}
81}
82
83@inproceedings
84{ chlipala:verified:2010,
85  author = {Adam Chlipala},
86  title = {A verified compiler for an impure functional language},
87  booktitle = {Proceedings of the $\mathrm{37^{th}}$ Annual Symposium on Principles of Programming Languages},
88  pages = {93--106},
89  year = {2010}
90}
91
92@inproceedings
93{ fox:trustworthy:2010,
94  author = {Anthony Fox and Magnus O. Myreen},
95  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
96  booktitle = {Proceedings of the $\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving},
97  pages = {243--258},
98  year = {2010}
99}
100
101@inproceedings
102{ garrigue:programming:1998,
103  author = {Jacques Garrigue},
104  title = {Programming with polymorphic variants},
105  booktitle = {{ML} Workshop},
106  year = {1998}
107}
108
109@inproceedings
110{ leijen:domain:1999,
111  author = {Daan Leijen and Erik Meijer},
112  title = {Domain specific embedded compilers},
113  booktitle = {Proceedings of the $\mathrm{2^{nd}}$ Conference on Domain Specific Languages},
114  pages = {109--122},
115  year = {1999}
116}
117
118@inproceedings
119{ sarkar:semantics:2009,
120  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},
121  title = {The semantics of {x86-CC} multiprocessor machine code},
122  booktitle = {Proceedings of the $\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},
123  pages = {379--391},
124  year = {2009}
125}
126
127@inproceedings
128{ shankar:principles:1999,
129  author = {Natarajan Shankar and Sam Owre},
130  title = {Principles and Pragmatics of Subtyping in {PVS}},
131  booktitle = {Recent Trends in Algebraic Development Techniques},
132  pages = {37--52},
133  year = {1999}
134}
135
136@inproceedings
137{ sozeau:subset:2006,
138  author = {Matthieu Sozeau},
139  title = {Subset coercions in {Coq}},
140  booktitle = {Proceedings of the Conference of the {TYPES} Project},
141  pages = {237--252},
142  year = {2006}
143}
144
145@inproceedings
146{ xi:guarded:2003,
147  author = {Hongwei Xi and Chiyan Chen and Gang Chen},
148  title = {Guarded recursive datatype constructors},
149  booktitle = {Proceedings of the $\mathrm{30^{th}}$ Annual Symposium on Principles of Programming Languages},
150  pages = {224--235},
151  year = {2003}
152}
153
154@misc
155{ cerco:2011,
156  title = {The {CerCo} {FET-Open} Project},
157  howpublished = {\url{http://cerco.cs.unibo.it}},
158  year = {2011},
159  key = {{CerCo}}
160}
161
162@misc
163{ cerco-code:2011,
164  title = {{CerCo Deliverable D4.1}: Matita and O'Caml code},
165  howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1_Code.tar.gz}},
166  year = {2011},
167  key = {{CerCo-code}}
168}
169
170@misc
171{ cerco-report:2011,
172  title = {{CerCo Deliverable D4.1}:: executable formal semantics of machine code},
173  howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1.pdf}},
174  year = {2011},
175  key = {{CerCo-report}}
176}
177
178@misc
179{ mcu8051ide:2010,
180  title = {{MCU 8051 IDE} 1.3.11},
181  howpublished = {\url{http://mcu8051ide.sourceforge.net/}},
182  year = {2010},
183  key = {{MCU}}
184}
185
186@misc
187{ oliboni:matita:2008,
188  author = {Cosimo A. Oliboni},
189  title = {{Matita} come Supporto per Specifiche Eseguibili: Formalizzazione Interattiva dei Microcontroller a 8 bit {Freescale}},
190  institution = {Dipartimento di Scienze dell'Informazione, Universit\`a di Bologna},
191  howpublished = {\url{http://matita.cs.unibo.it/library.shtml}},
192  year = {2008}
193}
194
195@misc
196{ sdcc:2010,
197  title = {Small Device {C} Compiler {(SDCC)} 3.0.0},
198  howpublished = {\url{http://sdcc.sourceforge.net/}},
199  year = {2010},
200  key = {{SDCC}}
201}
202
203@misc
204{ siemens:2011,
205  title = {{Siemens Semiconductor Group} 8051 derivative instruction set},
206  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
207  year = {2011},
208  key = {{Siemens}}
209}
210
211@techreport
212{ amadio:certifying:2010,
213  author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
214  title = {Cerifying cost annotations in compilers},
215  institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
216  year = {2010}
217}
Note: See TracBrowser for help on using the repository browser.