Ignore:
Timestamp:
Jun 21, 2011, 12:47:27 PM (8 years ago)
Author:
mulligan
Message:

final version? under 16 pages

File:
1 edited

Legend:

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

    r1020 r1026  
    33  author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli},
    44  title = {User interaction with the {Matita} proof assistant},
    5   journal = {Journal of Automated Reasoning},
     5  journal = {Automated Reasoning},
    66  pages = {109--139},
    77  volume = {39},
     
    2525  author = {Gerwin Klein and Tobias Nipkow},
    2626  title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
    27   journal = {Transactions on Programming Languages and Systems},
     27  journal = {{TOPLAS}},
    2828  volume = {28},
    2929  number = {4},
     
    3636  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},
    3737  title = {{seL4}: Formal verification of an operating system kernel},
    38   journal = {Communications of the {ACM}},
     38  journal = {{CACM}},
    3939  issue = {6},
    4040  volume = {53},
     
    4747  author = {Xavier Leroy},
    4848  title = {Formal verification of a realistic compiler},
    49   journal = {Communications of the {Association of Computing Machinery}},
     49  journal = {{CACM}},
    5050  volume = {52},
    5151  number = {7},
     
    5858  author = {Xavier Leroy},
    5959  title = {A formally verified compiler back-end},
    60   journal = {Journal of Automated Reasoning},
     60  journal = {Automated Reasoning},
    6161  volume = {43},
    6262  number = {4},
     
    8080  author = {Robert Atkey},
    8181  title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
    82   booktitle = {Conference of the {TYPES} Project},
     82  booktitle = {{TYPES}},
    8383  pages = {18--32},
    8484  year = {2007}
     
    8989  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
    9090  title = {Formal Verification of a {C} Compiler Front-End},
    91   booktitle = {International Symposium on Formal Methods},
     91  booktitle = {{FM}},
    9292  pages = {460--475},
    9393  year = {2006}
     
    9898  author = {Anthony Fox and Magnus O. Myreen},
    9999  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
    100   booktitle = {$\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving},
     100  booktitle = {{ITP}},
    101101  pages = {243--258},
    102102  year = {2010}
     
    107107  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},
    108108  title = {{seL4}: Formal verification of an operating system kernel},
    109   booktitle = {Proceedings of the $22^\mathrm{nd}$ {ACM} Symposium on Operating Systems Principles},
     109  booktitle = {{SOSP}},
    110110  year = {2009}
    111111}
     
    115115  author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
    116116  title = {An executable formal semantics of the {MCS-51} microprocessor in {Matita}},
    117   booktitle = {Formal Methods in Computer Aided Design},
     117  booktitle = {{FMCAD}},
    118118  year = {2011},
    119119  note = {Submitted}
     
    124124  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},
    125125  title = {The semantics of {x86-CC} multiprocessor machine code},
    126   booktitle = {$\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},
     126  booktitle = {{POPL}},
    127127  pages = {379--391},
    128128  year = {2009}
     
    133133  author = {Matthieu Sozeau},
    134134  title = {Subset Coercions in {Coq}},
    135   booktitle = {Types for Proofs and Programs},
     135  booktitle = {{TYPES}},
    136136  pages = {237--252},
    137137  year = {2006}
     
    142142  author = {Jun Yan and Wei Zhang},
    143143  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
    144   booktitle = {$\mathrm{14^{th}}$ {IEEE} Symposium on Real-time and Embedded Technology and Applications},
     144  booktitle = {{RTAS}},
    145145  pages = {80--89},
    146146  year = {2008}
     
    218218
    219219}
    220 
    221 @inproceedings{russell,
    222   author    = {Matthieu Sozeau},
    223   title     = {Subset Coercions in {C}oq},
    224   booktitle = {Types for Proofs and Programs},
    225   series    = {LNCS},
    226   year      = {2006},
    227   pages     = {237-252},
    228   VOLUME = {4502/2007},
    229   PUBLISHER = {Springer-Verlag},
    230   doi = {10.1007/978-3-540-74464-1\_16},
    231 }
Note: See TracChangeset for help on using the changeset viewer.