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

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

more added to bibliography

File size: 3.1 KB
Line 
1@article
2{ leroy:formal:2009,
3  author = {Xavier Leroy},
4  title = {Formal verification of a realistic compiler},
5  journal = {Communications of the {Association of Computing Machinery}},
6  volume = {52},
7  number = {7},
8  pages = {107--115},
9  year = {2009}
10}
11
12@article
13{ leroy:formally:2009,
14  author = {Xavier Leroy},
15  title = {A formally verified compiler back-end},
16  journal = {Journal of Automated Reasoning},
17  volume = {43},
18  number = {4},
19  pages = {363--446},
20  year = {2009}
21}
22
23@inproceedings
24{ atkey:coqjvm:2007,
25  author = {Robert Atkey},
26  title = {{CoqJVM}: An executable specification of the Java virtual machine using dependent types},
27  booktitle = {Proceedings of the Conference of the {TYPES} Project {(TYPES 2007)}},
28  pages = {18--32},
29  series = {Lecture Noted in Computer Science},
30  volume = {4941},
31  year = {2007}
32}
33
34@inproceedings
35{ blazy:formal:2006,
36  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
37  title = {Formal Verification of a {C} Compiler Front-End},
38  booktitle = {Proceedings of the International Symposium on Formal Methods ({FM 2006})},
39  series = {Lecture Notes in Computer Science},
40  volume = {4085},
41  pages = {460--475},
42  year = {2006}
43}
44
45@inproceedings
46{ chlipala:verified:2010,
47  author = {Adam Chlipala},
48  title = {A verified compiler for an impure functional language},
49  booktitle = {Proceedings of the Thirty Seventh Annual Symposium on Principles of Programming Languages {(POPL 2010)}},
50  series = {{ACM SIGPLAN} Notices},
51  volume = {45},
52  issue = {1},
53  pages = {93--106},
54  year = {2010}
55}
56
57@inproceedings
58{ fox:trustworthy:2010,
59  author = {Anthony Fox and Magnus O. Myreen},
60  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
61  booktitle = {Proceedings of the First International Conference on Interactive Theorem Proving ({ITP 2010})},
62  series = {Lecture Notes in Computer Science},
63  pages = {243--258},
64  year = {2010}
65}
66
67@inproceedings
68{ sarkar:semantics:2009,
69  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},
70  title = {The semantics of {x86-CC} multiprocessor machine code},
71  booktitle = {Proceedings of the Thirty Sixth Annual Symposium on Principles of Programming Languages {(POPL 2009)}},
72  series = {{ACM SIGPLAN} Notices},
73  pages = {379--391},
74  volume = {44},
75  issue = {1},
76  year = {2009}
77}
78
79@misc
80{ cerco:2011,
81  title = {The {CerCo} {FeT-Open} Project},
82  howpublished = {\url{http://cerco.cs.unibo.it}},
83  year = {2011},
84  key = {{CerCo}}
85}
86
87@misc
88{ mcu8051ide:2010,
89  title = {{MCU 8051 IDE} 1.3.11},
90  howpublished = {\url{http://mcu8051ide.sourceforge.net/}},
91  year = {2010},
92  key = {{MCU}}
93}
94
95@misc
96{ sdcc:2010,
97  title = {Small Device {C} Compiler {(SDCC)} 3.0.0},
98  howpublished = {\url{http://sdcc.sourceforge.net/}},
99  year = {2010},
100  key = {{SDCC}}
101}
102
103@techreport
104{ amadio:certifying:2010,
105  author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
106  title = {Cerifying cost annotations in compilers},
107  institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
108  year = {2010}
109}
Note: See TracBrowser for help on using the repository browser.