Ignore:
Timestamp:
Sep 9, 2011, 9:49:44 AM (8 years ago)
Author:
mulligan
Message:

got paper down to 15 and a half pages with nothing much added to document

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.bib

    r819 r1199  
    11@article
    22{ asperti:user:2007,
    3   author = {Andrea Asperti and Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli},
     3  author = {A. Asperti and C. Sacerdoti Coen and E. Tassi and S. 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},
     
    1212@article
    1313{ bate:wcet:2011,
    14   author = {Iain Bate and Usman Khan},
     14  author = {I. Bate and U. Khan},
    1515  title = {{WCET} analysis of modern processors using multi-criteria optimisation},
    1616  journal = {Empirical Software Engineering},
     
    2323@article
    2424{ leroy:formal:2009,
    25   author = {Xavier Leroy},
     25  author = {X. Leroy},
    2626  title = {Formal verification of a realistic compiler},
    27   journal = {Communications of the {Association of Computing Machinery}},
     27  journal = {CACM},
    2828  volume = {52},
    2929  number = {7},
     
    3434@article
    3535{ leroy:formally:2009,
    36   author = {Xavier Leroy},
     36  author = {X. Leroy},
    3737  title = {A formally verified compiler back-end},
    38   journal = {Journal of Automated Reasoning},
     38  journal = {Automated Reasoning},
    3939  volume = {43},
    4040  number = {4},
     
    4545@article
    4646{ luo:coercive:1999,
    47   author = {Zhaohui Luo},
     47  author = {Z. Luo},
    4848  title = {Coercive subtyping},
    49   journal = {Journal of Logic and Computation},
     49  journal = {Logic and Computation},
    5050  volume = {9},
    5151  number = {1},
     
    5656@inproceedings
    5757{ yan:wcet:2008,
    58   author = {Jun Yan and Wei Zhang},
     58  author = {J. Yan and W. Zhang},
    5959  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
    60   booktitle = {$\mathrm{14^{th}}$ {IEEE} Symposium on Real-time and Embedded Technology and Applications},
     60  booktitle = {{RTAS}},
    6161  pages = {80--89},
    6262  year = {2008}
     
    6565@inproceedings
    6666{ atkey:coqjvm:2007,
    67   author = {Robert Atkey},
     67  author = {R. Atkey},
    6868  title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
    69   booktitle = {Conference of the {TYPES} Project},
     69  booktitle = {{TYPES}},
    7070  pages = {18--32},
    7171  year = {2007}
     
    7575{ blanqui:designing:2010,
    7676  title = {Designing a {CPU} model: from a pseudo-formal document to fast code},
    77   author = {Fr\'ed\'eric Blanqui and Claude Helmstetter and Vania Joloboff and Jean-Fran\c{c}ois Monin and Xiaomu Shi},
    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}},
    7979  year = {2010}
    8080}
     
    8282@inproceedings
    8383{ blazy:formal:2006,
    84   author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
     84  author = {S. Blazy and Z. Dargaye and X. Leroy},
    8585  title = {Formal Verification of a {C} Compiler Front-End},
    86   booktitle = {International Symposium on Formal Methods},
     86  booktitle = {FM},
    8787  pages = {460--475},
    8888  year = {2006}
     
    9191@inproceedings
    9292{ chlipala:verified:2010,
    93   author = {Adam Chlipala},
     93  author = {A. Chlipala},
    9494  title = {A verified compiler for an impure functional language},
    95   booktitle = {$\mathrm{37^{th}}$ Annual Symposium on Principles of Programming Languages},
     95  booktitle = {POPL},
    9696  pages = {93--106},
    9797  year = {2010}
     
    100100@inproceedings
    101101{ fox:trustworthy:2010,
    102   author = {Anthony Fox and Magnus O. Myreen},
     102  author = {A. Fox and M. O. Myreen},
    103103  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},
    105105  pages = {243--258},
    106106  year = {2010}
     
    109109@inproceedings
    110110{ garrigue:programming:1998,
    111   author = {Jacques Garrigue},
     111  author = {J. Garrigue},
    112112  title = {Programming with polymorphic variants},
    113113  booktitle = {{ML} Workshop},
     
    117117@inproceedings
    118118{ leijen:domain:1999,
    119   author = {Daan Leijen and Erik Meijer},
     119  author = {D. Leijen and E. Meijer},
    120120  title = {Domain specific embedded compilers},
    121   booktitle = {$\mathrm{2^{nd}}$ Conference on Domain Specific Languages},
     121  booktitle = {DSL},
    122122  pages = {109--122},
    123123  year = {1999}
     
    126126@inproceedings
    127127{ sarkar:semantics:2009,
    128   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},
     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},
    129129  title = {The semantics of {x86-CC} multiprocessor machine code},
    130   booktitle = {$\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},
     130  booktitle = {POPL},
    131131  pages = {379--391},
    132132  year = {2009}
     
    135135@inproceedings
    136136{ shankar:principles:1999,
    137   author = {Natarajan Shankar and Sam Owre},
     137  author = {N. Shankar and S. Owre},
    138138  title = {Principles and Pragmatics of Subtyping in {PVS}},
    139139  booktitle = {Recent Trends in Algebraic Development Techniques},
     
    144144@inproceedings
    145145{ sozeau:subset:2006,
    146   author = {Matthieu Sozeau},
     146  author = {M. Sozeau},
    147147  title = {Subset coercions in {Coq}},
    148   booktitle = {Conference of the {TYPES} Project},
     148  booktitle = {{TYPES}},
    149149  pages = {237--252},
    150150  year = {2006}
     
    153153@inproceedings
    154154{ xi:guarded:2003,
    155   author = {Hongwei Xi and Chiyan Chen and Gang Chen},
     155  author = {H. Xi and C. Chen and G. Chen},
    156156  title = {Guarded recursive datatype constructors},
    157   booktitle = {$\mathrm{30^{th}}$ Annual Symposium on Principles of Programming Languages},
     157  booktitle = {POPL},
    158158  pages = {224--235},
    159159  year = {2003}
     
    162162@misc
    163163{ cerco:2011,
    164   title = {The {CerCo} {FET-Open} Project},
     164  title = {The {CerCo} Project},
    165165  howpublished = {\url{http://cerco.cs.unibo.it}},
    166166  year = {2011},
     
    186186@misc
    187187{ moore:grand:2005,
    188   author = {J Strother Moore},
     188  author = {J S. Moore},
    189189  title = {A Grand Challenge Proposal for Formal Methods},
    190190  year = {2005}
     
    193193@misc
    194194{ oliboni:matita:2008,
    195   author = {Cosimo A. Oliboni},
     195  author = {C. A. Oliboni},
    196196  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},
    198198  howpublished = {\url{http://matita.cs.unibo.it/library.shtml}},
    199199  year = {2008}
     
    218218@techreport
    219219{ amadio:certifying:2010,
    220   author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gis-Gianas and Ronan Saillard},
     220  author = {R. M. Amadio and N. Ayache and Y. R\'{e}gis-Gianas and R. Saillard},
    221221  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.