source: Papers/cpp-policy-2012/biblio.bib @ 3425

@article{Szymanski1978,
 author = {Szymanski, Thomas G.},
 title = {Assembling code for machines with span-dependent instructions},
 journal = {Commun. ACM},
 issue_date = {April 1978},
 volume = {21},
 number = {4},
 month = apr,
 year = {1978},
 issn = {0001-0782},
 pages = {300--308},
 numpages = {9},
 url = {http://doi.acm.org/10.1145/359460.359474},
 doi = {10.1145/359460.359474},
 acmid = {359474},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {NP-complete, assemblers, code generation, compilers, computational complexity, span-dependent instructions, variable-length addressing},
} 

@article{Robertson1979,
 author = {Robertson, Edward L.},
 title = {Code Generation and Storage Allocation for Machines with Span-Dependent Instructions},
 journal = {ACM Trans. Program. Lang. Syst.},
 issue_date = {July 1979},
 volume = {1},
 number = {1},
 month = jan,
 year = {1979},
 issn = {0164-0925},
 pages = {71--83},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/357062.357067},
 doi = {10.1145/357062.357067},
 acmid = {357067},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

@article{Dickson2008,
  author    = {Neil G. Dickson},
  title     = {A Simple, Linear-Time Algorithm for x86 Jump Encoding},
  journal   = {CoRR},
  volume    = {abs/0812.4973},
  year      = {2008},
  ee        = {http://arxiv.org/abs/0812.4973},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Sozeau2006,
  author = {Matthieu Sozeau},
  title = {Subset Coercions in {Coq}},
  booktitle = {{TYPES}},
  pages = {237--252},
  year = {2006}
}

@misc{SDCC2011,
  title = {Small Device {C} Compiler 3.1.0},
  howpublished = {\url{http://sdcc.sourceforge.net/}},
  year = {2011},
        key = {SDCC2011}
}

@misc{GCC2012,
        title = {GNU Compiler Collection 4.7.0},
        howpublished = {\url{http://gcc.gnu.org/}},
        year = {2012},
        key = {GCC2012}
}

@misc{IntelDev,
        author = {Intel},
        title = {{Intel 64 and IA-32 Architectures Developer's Manual}},
        howpublished={\url{http://www.intel.com/content/www/us/en/processors/architectures-software-developer-manuals.html}},
        volume=2,
  key = {IntelDev}
}

@article {Leroy2009,
   author = {Leroy, Xavier},
   affiliation = {INRIA Paris-Rocquencourt B.P. 105 78153 Le Chesnay France},
   title = {A Formally Verified Compiler Back-end},
   journal = {Journal of Automated Reasoning},
   publisher = {Springer Netherlands},
   issn = {0168-7433},
   keyword = {Computer Science},
   pages = {363-446},
   volume = {43},
   issue = {4},
   url = {http://dx.doi.org/10.1007/s10817-009-9155-4},
   note = {10.1007/s10817-009-9155-4},
   year = {2009}
}

@book {Moore1996, 
  author = {J Strother Moore},
  title = {Piton: A mechanically verified assembly language},
  series = {Automated Reasoning Series},
  volume = {3},
  isbn = {978-0-7923-3920-5},
  publisher = {Springer},
  year = {1996}
}

@misc {Hyde2006,
  title = {Branch displacement optimisation},
        author = {Randall Hyde},
  howpublished = {\url{http://groups.google.com/group/alt.lang.asm/msg/d31192d442accad3}},
  year = {2006},
}

@misc{DC2012,
        title={{On the correctness of an optimising assembler for the Intel MCS-51 microprocessor}},
        author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
        year = {2012},
        booktitle = {Certified Proofs and Programs {(CPP)}},
        note = {Submitted}
}

@article{Asperti2007,
  author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli},
  title = {User interaction with the {Matita} proof assistant},
  journal = {Automated Reasoning},
  pages = {109--139},
  volume = {39},
  issue = {2},
  year = {2007}
}

@article{TSO2011,
 author = {\v{S}ev\v{c}ik, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
 title = {Relaxed-memory concurrency and verified compilation},
 journal = {SIGPLAN Not.},
 issue_date = {January 2011},
 volume = {46},
 number = {1},
 month = jan,
 year = {2011},
 issn = {0362-1340},
 pages = {43--54},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1925844.1926393},
 doi = {10.1145/1925844.1926393},
 acmid = {1926393},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {relaxed memory models, semantics, verifying compilation},
} 

@inproceedings{Sevcik:2011:RCV:1926385.1926393,
 author = {\v{S}ev\v{c}ik, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
 title = {Relaxed-memory concurrency and verified compilation},
 booktitle = {Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 series = {POPL '11},
 year = {2011},
 isbn = {978-1-4503-0490-0},
 location = {Austin, Texas, USA},
 pages = {43--54},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1926385.1926393},
 doi = {10.1145/1926385.1926393},
 acmid = {1926393},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {relaxed memory models, semantics, verifying compilation},
}