Ignore:
Timestamp:
Jun 16, 2011, 2:39:23 PM (9 years ago)
Author:
mulligan
Message:

added more, worked on conclusions and related work. need just to finish explanation of large lemmas

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.bib

    r970 r981  
    2222
    2323@article
     24{ klein:machine:2006,
     25  author = {Gerwin Klein and Tobias Nipkow},
     26  title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
     27  journal = {Transactions on Programming Languages and Systems},
     28  volume = {28},
     29  number = {4},
     30  pages = {619--695},
     31  year = {2006}
     32}
     33
     34@article
    2435{ klein:sel4:2010,
    2536  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},
     
    5465}
    5566
     67@book
     68{ moore:piton:1996,
     69  author = {J Strother Moore},
     70  title = {Piton: A mechanically verified assembly language},
     71  series = {Automated Reasoning Series},
     72  volume = {3},
     73  isbn = {978-0-7923-3920-5},
     74  publisher = {Springer},
     75  year = {1996}
     76}
     77
     78@inproceedings
     79{ atkey:coqjvm:2007,
     80  author = {Robert Atkey},
     81  title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
     82  booktitle = {Conference of the {TYPES} Project},
     83  pages = {18--32},
     84  year = {2007}
     85}
     86
    5687@inproceedings
    5788{ blazy:formal:2006,
     
    6495
    6596@inproceedings
     97{ fox:trustworthy:2010,
     98  author = {Anthony Fox and Magnus O. Myreen},
     99  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
     100  booktitle = {$\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving},
     101  pages = {243--258},
     102  year = {2010}
     103}
     104
     105@inproceedings
    66106{ klein:sel4:2009,
    67107  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},
     
    78118  year = {2011},
    79119  note = {Submitted}
     120}
     121
     122@inproceedings
     123{ sarkar:semantics:2009,
     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},
     125  title = {The semantics of {x86-CC} multiprocessor machine code},
     126  booktitle = {$\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},
     127  pages = {379--391},
     128  year = {2009}
     129}
     130
     131@inproceedings
     132{ sozeau:subset:2006,
     133  author = {Matthieu Sozeau},
     134  title = {Subset Coercions in {Coq}},
     135  booktitle = {Types for Proofs and Programs},
     136  pages = {237--252},
     137  year = {2006}
    80138}
    81139
     
    114172
    115173@misc
     174{ moore:grand:2005,
     175  author = {J Strother Moore},
     176  title = {A Grand Challenge Proposal for Formal Methods},
     177  year = {2005}
     178}
     179
     180@misc
    116181{ sdcc:2011,
    117182  title = {Small Device {C} Compiler 3.0.0},
     
    143208  year = {2010}
    144209}
     210
     211@techreport
     212{ klein:machine:2010,
     213  author = {Gerwin Klein and Tobias Nipkow},
     214  title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
     215  institution = {National {ICT} Australia},
     216  number = {0400001T.1},
     217  year = {2010}
     218
     219}
Note: See TracChangeset for help on using the changeset viewer.