Changeset 1026 for src/ASM/CPP2011/cpp-2011.bib

Timestamp:

Jun 21, 2011, 12:47:27 PM (9 years ago)

Author:

mulligan

Message:

final version? under 16 pages

File:

• src/ASM/CPP2011/cpp-2011.bib (modified) (14 diffs)

src/ASM/CPP2011/cpp-2011.bib

@@ -3 +3 @@
   author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli},
   title = {User interaction with the {Matita} proof assistant},
-  journal = {Journal of Automated Reasoning},
+  journal = {Automated Reasoning},
   pages = {109--139},
   volume = {39},
@@ -25 +25 @@
   author = {Gerwin Klein and Tobias Nipkow},
   title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
-  journal = {Transactions on Programming Languages and Systems},
+  journal = {{TOPLAS}},
   volume = {28}, 
   number = {4}, 
@@ -36 +36 @@
   author = {Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell, Harvey Tuch and Simon Winwood},
   title = {{seL4}: Formal verification of an operating system kernel},
-  journal = {Communications of the {ACM}},
+  journal = {{CACM}},
   issue = {6},
   volume = {53},
@@ -47 +47 @@
   author = {Xavier Leroy},
   title = {Formal verification of a realistic compiler},
-  journal = {Communications of the {Association of Computing Machinery}},
+  journal = {{CACM}},
   volume = {52},
   number = {7},
@@ -58 +58 @@
   author = {Xavier Leroy},
   title = {A formally verified compiler back-end},
-  journal = {Journal of Automated Reasoning},
+  journal = {Automated Reasoning},
   volume = {43},
   number = {4},
@@ -80 +80 @@
   author = {Robert Atkey},
   title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
-  booktitle = {Conference of the {TYPES} Project},
+  booktitle = {{TYPES}},
   pages = {18--32},
   year = {2007}
@@ -89 +89 @@
   author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
   title = {Formal Verification of a {C} Compiler Front-End},
-  booktitle = {International Symposium on Formal Methods},
+  booktitle = {{FM}},
   pages = {460--475},
   year = {2006}
@@ -98 +98 @@
   author = {Anthony Fox and Magnus O. Myreen},
   title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
-  booktitle = {$\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving},
+  booktitle = {{ITP}},
   pages = {243--258},
   year = {2010}
@@ -107 +107 @@
   author = {Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell, Harvey Tuch and Simon Winwood},
   title = {{seL4}: Formal verification of an operating system kernel},
-  booktitle = {Proceedings of the $22^\mathrm{nd}$ {ACM} Symposium on Operating Systems Principles},
+  booktitle = {{SOSP}},
   year = {2009}
 }
@@ -115 +115 @@
   author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
   title = {An executable formal semantics of the {MCS-51} microprocessor in {Matita}},
-  booktitle = {Formal Methods in Computer Aided Design},
+  booktitle = {{FMCAD}},
   year = {2011},
   note = {Submitted}
@@ -124 +124 @@
   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},
   title = {The semantics of {x86-CC} multiprocessor machine code},
-  booktitle = {$\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},
+  booktitle = {{POPL}},
   pages = {379--391},
   year = {2009}
@@ -133 +133 @@
   author = {Matthieu Sozeau},
   title = {Subset Coercions in {Coq}},
-  booktitle = {Types for Proofs and Programs},
+  booktitle = {{TYPES}},
   pages = {237--252},
   year = {2006}
@@ -142 +142 @@
   author = {Jun Yan and Wei Zhang},
   title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
-  booktitle = {$\mathrm{14^{th}}$ {IEEE} Symposium on Real-time and Embedded Technology and Applications},
+  booktitle = {{RTAS}},
   pages = {80--89},
   year = {2008}
@@ -218 +218 @@
 
 }
-
-@inproceedings{russell,
-  author    = {Matthieu Sozeau},
-  title     = {Subset Coercions in {C}oq},
-  booktitle = {Types for Proofs and Programs},
-  series    = {LNCS},
-  year      = {2006},
-  pages     = {237-252},
-  VOLUME = {4502/2007},
-  PUBLISHER = {Springer-Verlag},
-  doi = {10.1007/978-3-540-74464-1\_16},
-}