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

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

slight tweaks

File size: 5.6 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@inproceedings
46{ yan:wcet:2008,
47  author = {Jun Yan and Wei Zhang},
48  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
49  booktitle = {Proceedings of the $\mathrm{14^{th}}$ {IEEE} Symposium on Real-time and Embedded Technology and Applications},
50  pages = {80--89},
51  year = {2008}
52}
53
54@inproceedings
55{ atkey:coqjvm:2007,
56  author = {Robert Atkey},
57  title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
58  booktitle = {Proceedings of the Conference of the {TYPES} Project},
59  pages = {18--32},
60  year = {2007}
61}
62
63@inproceedings
64{ blazy:formal:2006,
65  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
66  title = {Formal Verification of a {C} Compiler Front-End},
67  booktitle = {Proceedings of the International Symposium on Formal Methods},
68  pages = {460--475},
69  year = {2006}
70}
71
72@inproceedings
73{ chlipala:verified:2010,
74  author = {Adam Chlipala},
75  title = {A verified compiler for an impure functional language},
76  booktitle = {Proceedings of the $\mathrm{37^{th}}$ Annual Symposium on Principles of Programming Languages},
77  pages = {93--106},
78  year = {2010}
79}
80
81@inproceedings
82{ fox:trustworthy:2010,
83  author = {Anthony Fox and Magnus O. Myreen},
84  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
85  booktitle = {Proceedings of the $\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving},
86  pages = {243--258},
87  year = {2010}
88}
89
90@inproceedings
91{ garrigue:programming:1998,
92  author = {Jacques Garrigue},
93  title = {Programming with polymorphic variants},
94  booktitle = {{ML} Workshop},
95  year = {1998}
96}
97
98@inproceedings
99{ leijen:domain:1999,
100  author = {Daan Leijen and Erik Meijer},
101  title = {Domain specific embedded compilers},
102  booktitle = {Proceedings of the $\mathrm{2^{nd}}$ Conference on Domain Specific Languages},
103  pages = {109--122},
104  year = {1999}
105}
106
107@inproceedings
108{ sarkar:semantics:2009,
109  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},
110  title = {The semantics of {x86-CC} multiprocessor machine code},
111  booktitle = {Proceedings of the $\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},
112  pages = {379--391},
113  year = {2009}
114}
115
116@inproceedings
117{ shankar:principles:1999,
118  author = {Natarajan Shankar and Sam Owre},
119  title = {Principles and Pragmatics of Subtyping in {PVS}},
120  booktitle = {Recent Trends in Algebraic Development Techniques},
121  pages = {37--52},
122  year = {1999}
123}
124
125@inproceedings
126{ sozeau:subset:2006,
127  author = {Matthieu Sozeau},
128  title = {Subset coercions in {Coq}},
129  booktitle = {Proceedings of the Conference of the {TYPES} Project},
130  pages = {237--252},
131  year = {2006}
132}
133
134@misc
135{ cerco:2011,
136  title = {The {CerCo} {FET-Open} Project},
137  howpublished = {\url{http://cerco.cs.unibo.it}},
138  year = {2011},
139  key = {{CerCo}}
140}
141
142@misc
143{ cerco-code:2011,
144  title = {{CerCo Deliverable D4.1}: Matita and O'Caml code},
145  howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1_Code.tar.gz}},
146  year = {2011},
147  key = {{CerCo-code}}
148}
149
150@misc
151{ cerco-report:2011,
152  title = {{CerCo Deliverable D4.1}:: executable formal semantics of machine code},
153  howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1.pdf}},
154  year = {2011},
155  key = {{CerCo-report}}
156}
157
158@misc
159{ mcu8051ide:2010,
160  title = {{MCU 8051 IDE} 1.3.11},
161  howpublished = {\url{http://mcu8051ide.sourceforge.net/}},
162  year = {2010},
163  key = {{MCU}}
164}
165
166@misc
167{ oliboni:matita:2008,
168  author = {Cosimo A. Oliboni},
169  title = {{Matita} come Supporto per Specifiche Eseguibili: Formalizzazione Interattiva dei Microcontroller a 8 bit {Freescale}},
170  institution = {Dipartimento di Scienze dell'Informazione, Universit\`a di Bologna},
171  howpublished = {\url{http://matita.cs.unibo.it/library.shtml}},
172  year = {2008}
173}
174
175@misc
176{ sdcc:2010,
177  title = {Small Device {C} Compiler {(SDCC)} 3.0.0},
178  howpublished = {\url{http://sdcc.sourceforge.net/}},
179  year = {2010},
180  key = {{SDCC}}
181}
182
183@misc
184{ siemens:2011,
185  title = {{Siemens Semiconductor Group} 8051 derivative instruction set},
186  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
187  year = {2011},
188  key = {{Siemens}}
189}
190
191@techreport
192{ amadio:certifying:2010,
193  author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
194  title = {Cerifying cost annotations in compilers},
195  institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
196  year = {2010}
197}
Note: See TracBrowser for help on using the repository browser.