source: Papers/itp-2011/itp-2011.bib @ 3558

@article
{ asperti:user:2007,
  author = {A. Asperti and C. Sacerdoti Coen and E. Tassi and S. Zacchiroli},
  title = {User interaction with the {Matita} proof assistant},
  journal = {Automated Reasoning},
  pages = {109--139},
  volume = {39},
  issue = {2},
  year = {2007}
}

@article
{ bate:wcet:2011,
  author = {I. Bate and U. Khan},
  title = {{WCET} analysis of modern processors using multi-criteria optimisation},
  journal = {Empirical Software Engineering},
  pages = {5--28},
  volume = {16},
  issue = {1},
  year = {2011}
}

@article
{ leroy:formal:2009,
  author = {X. Leroy},
  title = {Formal verification of a realistic compiler},
  journal = {CACM},
  volume = {52},
  number = {7},
  pages = {107--115},
  year = {2009}
}

@article
{ leroy:formally:2009,
  author = {X. Leroy},
  title = {A formally verified compiler back-end},
  journal = {Automated Reasoning},
  volume = {43},
  number = {4},
  pages = {363--446},
  year = {2009}
}

@article
{ luo:coercive:1999,
  author = {Z. Luo},
  title = {Coercive subtyping},
  journal = {Logic and Computation},
  volume = {9},
  number = {1},
  pages = {105--130},
  year = {1999}
}

@inproceedings
{ myreen:extensible:2009,
  author = {M. O. Myreen and K. Slind and Michael J. C. Gordon},
  title = {Extensible proof-producing compilation},
  booktitle = {CC},
  volume = {5501},
  pages = {2--16},
  year = {2009}
}

@inproceedings
{ hunt:verifying:2010,
  author = {W. A. Hunt Jr.},
  title = {Verifying {VIA Nano} microprocessor components},
  booktitle = {FMCAD},
  year = {2010}
}

@inproceedings
{ yan:wcet:2008,
  author = {J. Yan and W. Zhang},
  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
  booktitle = {{RTAS}},
  pages = {80--89},
  year = {2008}
}

@inproceedings
{ atkey:coqjvm:2007,
  author = {R. Atkey},
  title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
  booktitle = {{TYPES}},
  pages = {18--32},
  year = {2007}
}

@inproceedings
{ blanqui:designing:2010,
  title = {Designing a {CPU} model: from a pseudo-formal document to fast code},
  author = {F. Blanqui and C. Helmstetter and V. Joloboff and J. Monin and X. Shi},
  booktitle = {{RAPIDO}},
  year = {2010}
}

@inproceedings
{ blazy:formal:2006,
  author = {S. Blazy and Z. Dargaye and X. Leroy},
  title = {Formal Verification of a {C} Compiler Front-End},
  booktitle = {FM},
  pages = {460--475},
  year = {2006}
}

@inproceedings
{ chlipala:verified:2010,
  author = {A. Chlipala},
  title = {A verified compiler for an impure functional language},
  booktitle = {POPL},
  pages = {93--106},
  year = {2010}
}

@inproceedings
{ fox:trustworthy:2010,
  author = {A. Fox and M. O. Myreen},
  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
  booktitle = {ITP},
  pages = {243--258},
  year = {2010}
}

@inproceedings
{ garrigue:programming:1998,
  author = {J. Garrigue},
  title = {Programming with polymorphic variants},
  booktitle = {{ML} Workshop},
  year = {1998}
}

@inproceedings
{ leijen:domain:1999,
  author = {D. Leijen and E. Meijer},
  title = {Domain specific embedded compilers},
  booktitle = {DSL},
  pages = {109--122},
  year = {1999}
}

@inproceedings
{ sarkar:semantics:2009,
  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},
  title = {The semantics of {x86-CC} multiprocessor machine code},
  booktitle = {POPL},
  pages = {379--391},
  year = {2009}
}

@inproceedings
{ shankar:principles:1999,
  author = {N. Shankar and S. Owre},
  title = {Principles and Pragmatics of Subtyping in {PVS}},
  booktitle = {Recent Trends in Algebraic Development Techniques},
  pages = {37--52},
  year = {1999}
}

@inproceedings
{ sozeau:subset:2006,
  author = {M. Sozeau},
  title = {Subset coercions in {Coq}},
  booktitle = {{TYPES}},
  pages = {237--252},
  year = {2006}
}

@inproceedings
{ xi:guarded:2003,
  author = {H. Xi and C. Chen and G. Chen},
  title = {Guarded recursive datatype constructors},
  booktitle = {POPL},
  pages = {224--235},
  year = {2003}
}

@misc
{ cerco:2011,
  title = {The {CerCo} Project},
  howpublished = {\url{http://cerco.cs.unibo.it}},
  year = {2011},
  key = {{CerCo}}
}

@misc
{ cerco-report-code:2011,
  title = {{CerCo Deliverable D4.1}: executable formal semantics of machine code},
  howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1.pdf} and \url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1_Code.tar.gz}},
  year = {2011},
  key = {{CerCo-report-code}}
}

@misc
{ mcu8051ide:2010,
  title = {{MCU 8051 IDE} 1.3.11},
  howpublished = {\url{http://mcu8051ide.sourceforge.net/}},
  year = {2010},
  key = {{MCU}}
}

@misc
{ moore:grand:2005,
  author = {J S. Moore},
  title = {A Grand Challenge Proposal for Formal Methods},
  year = {2005}
}

@misc
{ oliboni:matita:2008,
  author = {C. A. Oliboni},
  title = {{Matita} come Supporto per Specifiche Eseguibili: Formalizzazione Interattiva dei Microcontroller a 8 bit {Freescale}},
  institution = {Universit\`a di Bologna},
  howpublished = {\url{http://matita.cs.unibo.it/library.shtml}},
  year = {2008}
}

@misc
{ sdcc:2010,
  title = {Small Device {C} Compiler 3.0.0},
  howpublished = {\url{http://sdcc.sourceforge.net/}},
  year = {2010},
  key = {{SDCC}}
}

@misc
{ siemens:2011,
  title = {{Siemens Semiconductor Group} 8051 derivative instruction set},
  howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instruction-set.pdf}},
  year = {2011},
  key = {{Siemens}}
}

@techreport
{ amadio:certifying:2010,
  author = {R. M. Amadio and N. Ayache and Y. R\'{e}gis-Gianas and R. Saillard},
  title = {Cerifying cost annotations in compilers},
  institution = {Universit\'{e} Paris Diderot},
  year = {2010}
}