Changeset 1026 for src/ASM/CPP2011/cpp-2011.bib
- Timestamp:
- Jun 21, 2011, 12:47:27 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CPP2011/cpp-2011.bib
r1020 r1026 3 3 author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli}, 4 4 title = {User interaction with the {Matita} proof assistant}, 5 journal = { Journal ofAutomated Reasoning},5 journal = {Automated Reasoning}, 6 6 pages = {109--139}, 7 7 volume = {39}, … … 25 25 author = {Gerwin Klein and Tobias Nipkow}, 26 26 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}}, 28 28 volume = {28}, 29 29 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}, 37 37 title = {{seL4}: Formal verification of an operating system kernel}, 38 journal = { Communications of the {ACM}},38 journal = {{CACM}}, 39 39 issue = {6}, 40 40 volume = {53}, … … 47 47 author = {Xavier Leroy}, 48 48 title = {Formal verification of a realistic compiler}, 49 journal = { Communications of the {Association of Computing Machinery}},49 journal = {{CACM}}, 50 50 volume = {52}, 51 51 number = {7}, … … 58 58 author = {Xavier Leroy}, 59 59 title = {A formally verified compiler back-end}, 60 journal = { Journal ofAutomated Reasoning},60 journal = {Automated Reasoning}, 61 61 volume = {43}, 62 62 number = {4}, … … 80 80 author = {Robert Atkey}, 81 81 title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types}, 82 booktitle = { Conference of the {TYPES} Project},82 booktitle = {{TYPES}}, 83 83 pages = {18--32}, 84 84 year = {2007} … … 89 89 author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy}, 90 90 title = {Formal Verification of a {C} Compiler Front-End}, 91 booktitle = { International Symposium on Formal Methods},91 booktitle = {{FM}}, 92 92 pages = {460--475}, 93 93 year = {2006} … … 98 98 author = {Anthony Fox and Magnus O. Myreen}, 99 99 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}}, 101 101 pages = {243--258}, 102 102 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}, 108 108 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}}, 110 110 year = {2009} 111 111 } … … 115 115 author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}}, 116 116 title = {An executable formal semantics of the {MCS-51} microprocessor in {Matita}}, 117 booktitle = { Formal Methods in Computer Aided Design},117 booktitle = {{FMCAD}}, 118 118 year = {2011}, 119 119 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}, 125 125 title = {The semantics of {x86-CC} multiprocessor machine code}, 126 booktitle = { $\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},126 booktitle = {{POPL}}, 127 127 pages = {379--391}, 128 128 year = {2009} … … 133 133 author = {Matthieu Sozeau}, 134 134 title = {Subset Coercions in {Coq}}, 135 booktitle = { Types for Proofs and Programs},135 booktitle = {{TYPES}}, 136 136 pages = {237--252}, 137 137 year = {2006} … … 142 142 author = {Jun Yan and Wei Zhang}, 143 143 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}}, 145 145 pages = {80--89}, 146 146 year = {2008} … … 218 218 219 219 } 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.