Changeset 1199 for Deliverables/D4.1/ITPPaper/itp2011.bib
 Timestamp:
 Sep 9, 2011, 9:49:44 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/ITPPaper/itp2011.bib
r819 r1199 1 1 @article 2 2 { asperti:user:2007, 3 author = {A ndrea Asperti and Claudio Sacerdoti Coen and Enrico Tassi and StefanoZacchiroli},3 author = {A. Asperti and C. Sacerdoti Coen and E. Tassi and S. Zacchiroli}, 4 4 title = {User interaction with the {Matita} proof assistant}, 5 journal = { Journal ofAutomated Reasoning},5 journal = {Automated Reasoning}, 6 6 pages = {109139}, 7 7 volume = {39}, … … 12 12 @article 13 13 { bate:wcet:2011, 14 author = {I ain Bate and UsmanKhan},14 author = {I. Bate and U. Khan}, 15 15 title = {{WCET} analysis of modern processors using multicriteria optimisation}, 16 16 journal = {Empirical Software Engineering}, … … 23 23 @article 24 24 { leroy:formal:2009, 25 author = {X avierLeroy},25 author = {X. Leroy}, 26 26 title = {Formal verification of a realistic compiler}, 27 journal = {C ommunications of the {Association of Computing Machinery}},27 journal = {CACM}, 28 28 volume = {52}, 29 29 number = {7}, … … 34 34 @article 35 35 { leroy:formally:2009, 36 author = {X avierLeroy},36 author = {X. Leroy}, 37 37 title = {A formally verified compiler backend}, 38 journal = { Journal ofAutomated Reasoning},38 journal = {Automated Reasoning}, 39 39 volume = {43}, 40 40 number = {4}, … … 45 45 @article 46 46 { luo:coercive:1999, 47 author = {Z haohuiLuo},47 author = {Z. Luo}, 48 48 title = {Coercive subtyping}, 49 journal = { Journal ofLogic and Computation},49 journal = {Logic and Computation}, 50 50 volume = {9}, 51 51 number = {1}, … … 56 56 @inproceedings 57 57 { yan:wcet:2008, 58 author = {J un Yan and WeiZhang},58 author = {J. Yan and W. Zhang}, 59 59 title = {{WCET} Analysis for MultiCore Processors with Shared {L2} Instruction Caches}, 60 booktitle = { $\mathrm{14^{th}}$ {IEEE} Symposium on Realtime and Embedded Technology and Applications},60 booktitle = {{RTAS}}, 61 61 pages = {8089}, 62 62 year = {2008} … … 65 65 @inproceedings 66 66 { atkey:coqjvm:2007, 67 author = {R obertAtkey},67 author = {R. Atkey}, 68 68 title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types}, 69 booktitle = { Conference of the {TYPES} Project},69 booktitle = {{TYPES}}, 70 70 pages = {1832}, 71 71 year = {2007} … … 75 75 { blanqui:designing:2010, 76 76 title = {Designing a {CPU} model: from a pseudoformal document to fast code}, 77 author = {F r\'ed\'eric Blanqui and Claude Helmstetter and Vania Joloboff and JeanFran\c{c}ois Monin and XiaomuShi},78 booktitle = { $\mathrm{3^{rd}}$ Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools},77 author = {F. Blanqui and C. Helmstetter and V. Joloboff and J. Monin and X. Shi}, 78 booktitle = {{RAPIDO}}, 79 79 year = {2010} 80 80 } … … 82 82 @inproceedings 83 83 { blazy:formal:2006, 84 author = {S andrine Blazy and Zaynah Dargaye and XavierLeroy},84 author = {S. Blazy and Z. Dargaye and X. Leroy}, 85 85 title = {Formal Verification of a {C} Compiler FrontEnd}, 86 booktitle = { International Symposium on Formal Methods},86 booktitle = {FM}, 87 87 pages = {460475}, 88 88 year = {2006} … … 91 91 @inproceedings 92 92 { chlipala:verified:2010, 93 author = {A damChlipala},93 author = {A. Chlipala}, 94 94 title = {A verified compiler for an impure functional language}, 95 booktitle = { $\mathrm{37^{th}}$ Annual Symposium on Principles of Programming Languages},95 booktitle = {POPL}, 96 96 pages = {93106}, 97 97 year = {2010} … … 100 100 @inproceedings 101 101 { fox:trustworthy:2010, 102 author = {A nthony Fox and MagnusO. Myreen},102 author = {A. Fox and M. O. Myreen}, 103 103 title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture}, 104 booktitle = { $\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving},104 booktitle = {ITP}, 105 105 pages = {243258}, 106 106 year = {2010} … … 109 109 @inproceedings 110 110 { garrigue:programming:1998, 111 author = {J acquesGarrigue},111 author = {J. Garrigue}, 112 112 title = {Programming with polymorphic variants}, 113 113 booktitle = {{ML} Workshop}, … … 117 117 @inproceedings 118 118 { leijen:domain:1999, 119 author = {D aan Leijen and ErikMeijer},119 author = {D. Leijen and E. Meijer}, 120 120 title = {Domain specific embedded compilers}, 121 booktitle = { $\mathrm{2^{nd}}$ Conference on Domain Specific Languages},121 booktitle = {DSL}, 122 122 pages = {109122}, 123 123 year = {1999} … … 126 126 @inproceedings 127 127 { sarkar:semantics:2009, 128 author = {S usmit Sarkar and Peter Sewell and Francesco Zappa Nardelli and Scott Owens and Tom Ridge and Thomas Braibant and Magnus O. Myreen and JadeAlglave},128 author = {S. Sarkar and P. Sewell and F. Zappa Nardelli and S. Owens and T. Ridge and T. Braibant and M. O. Myreen and J. Alglave}, 129 129 title = {The semantics of {x86CC} multiprocessor machine code}, 130 booktitle = { $\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},130 booktitle = {POPL}, 131 131 pages = {379391}, 132 132 year = {2009} … … 135 135 @inproceedings 136 136 { shankar:principles:1999, 137 author = {N atarajan Shankar and SamOwre},137 author = {N. Shankar and S. Owre}, 138 138 title = {Principles and Pragmatics of Subtyping in {PVS}}, 139 139 booktitle = {Recent Trends in Algebraic Development Techniques}, … … 144 144 @inproceedings 145 145 { sozeau:subset:2006, 146 author = {M atthieuSozeau},146 author = {M. Sozeau}, 147 147 title = {Subset coercions in {Coq}}, 148 booktitle = { Conference of the {TYPES} Project},148 booktitle = {{TYPES}}, 149 149 pages = {237252}, 150 150 year = {2006} … … 153 153 @inproceedings 154 154 { xi:guarded:2003, 155 author = {H ongwei Xi and Chiyan Chen and GangChen},155 author = {H. Xi and C. Chen and G. Chen}, 156 156 title = {Guarded recursive datatype constructors}, 157 booktitle = { $\mathrm{30^{th}}$ Annual Symposium on Principles of Programming Languages},157 booktitle = {POPL}, 158 158 pages = {224235}, 159 159 year = {2003} … … 162 162 @misc 163 163 { cerco:2011, 164 title = {The {CerCo} {FETOpen}Project},164 title = {The {CerCo} Project}, 165 165 howpublished = {\url{http://cerco.cs.unibo.it}}, 166 166 year = {2011}, … … 186 186 @misc 187 187 { moore:grand:2005, 188 author = {J S trotherMoore},188 author = {J S. Moore}, 189 189 title = {A Grand Challenge Proposal for Formal Methods}, 190 190 year = {2005} … … 193 193 @misc 194 194 { oliboni:matita:2008, 195 author = {C osimoA. Oliboni},195 author = {C. A. Oliboni}, 196 196 title = {{Matita} come Supporto per Specifiche Eseguibili: Formalizzazione Interattiva dei Microcontroller a 8 bit {Freescale}}, 197 institution = { Dipartimento di Scienze dell'Informazione,Universit\`a di Bologna},197 institution = {Universit\`a di Bologna}, 198 198 howpublished = {\url{http://matita.cs.unibo.it/library.shtml}}, 199 199 year = {2008} … … 218 218 @techreport 219 219 { amadio:certifying:2010, 220 author = {R oberto M. Amadio and Nicolas Ayache and Yann R\'{e}gisGianas and RonanSaillard},220 author = {R. M. Amadio and N. Ayache and Y. R\'{e}gisGianas and R. Saillard}, 221 221 title = {Cerifying cost annotations in compilers}, 222 institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},223 year = {2010} 224 } 222 institution = {Universit\'{e} Paris Diderot}, 223 year = {2010} 224 }
Note: See TracChangeset
for help on using the changeset viewer.