| 1 | @article{Szymanski1978, |
|---|
| 2 | author = {Szymanski, Thomas G.}, |
|---|
| 3 | title = {Assembling code for machines with span-dependent instructions}, |
|---|
| 4 | journal = {Commun. ACM}, |
|---|
| 5 | issue_date = {April 1978}, |
|---|
| 6 | volume = {21}, |
|---|
| 7 | number = {4}, |
|---|
| 8 | month = apr, |
|---|
| 9 | year = {1978}, |
|---|
| 10 | issn = {0001-0782}, |
|---|
| 11 | pages = {300--308}, |
|---|
| 12 | numpages = {9}, |
|---|
| 13 | url = {http://doi.acm.org/10.1145/359460.359474}, |
|---|
| 14 | doi = {10.1145/359460.359474}, |
|---|
| 15 | acmid = {359474}, |
|---|
| 16 | publisher = {ACM}, |
|---|
| 17 | address = {New York, NY, USA}, |
|---|
| 18 | keywords = {NP-complete, assemblers, code generation, compilers, computational complexity, span-dependent instructions, variable-length addressing}, |
|---|
| 19 | } |
|---|
| 20 | |
|---|
| 21 | @article{Robertson1979, |
|---|
| 22 | author = {Robertson, Edward L.}, |
|---|
| 23 | title = {Code Generation and Storage Allocation for Machines with Span-Dependent Instructions}, |
|---|
| 24 | journal = {ACM Trans. Program. Lang. Syst.}, |
|---|
| 25 | issue_date = {July 1979}, |
|---|
| 26 | volume = {1}, |
|---|
| 27 | number = {1}, |
|---|
| 28 | month = jan, |
|---|
| 29 | year = {1979}, |
|---|
| 30 | issn = {0164-0925}, |
|---|
| 31 | pages = {71--83}, |
|---|
| 32 | numpages = {13}, |
|---|
| 33 | url = {http://doi.acm.org/10.1145/357062.357067}, |
|---|
| 34 | doi = {10.1145/357062.357067}, |
|---|
| 35 | acmid = {357067}, |
|---|
| 36 | publisher = {ACM}, |
|---|
| 37 | address = {New York, NY, USA}, |
|---|
| 38 | } |
|---|
| 39 | |
|---|
| 40 | @article{Dickson2008, |
|---|
| 41 | author = {Neil G. Dickson}, |
|---|
| 42 | title = {A Simple, Linear-Time Algorithm for x86 Jump Encoding}, |
|---|
| 43 | journal = {CoRR}, |
|---|
| 44 | volume = {abs/0812.4973}, |
|---|
| 45 | year = {2008}, |
|---|
| 46 | ee = {http://arxiv.org/abs/0812.4973}, |
|---|
| 47 | bibsource = {DBLP, http://dblp.uni-trier.de} |
|---|
| 48 | } |
|---|
| 49 | |
|---|
| 50 | @inproceedings{Sozeau2006, |
|---|
| 51 | author = {Matthieu Sozeau}, |
|---|
| 52 | title = {Subset Coercions in {Coq}}, |
|---|
| 53 | booktitle = {{TYPES}}, |
|---|
| 54 | pages = {237--252}, |
|---|
| 55 | year = {2006} |
|---|
| 56 | } |
|---|
| 57 | |
|---|
| 58 | @misc{SDCC2011, |
|---|
| 59 | title = {Small Device {C} Compiler 3.1.0}, |
|---|
| 60 | howpublished = {\url{http://sdcc.sourceforge.net/}}, |
|---|
| 61 | year = {2011} |
|---|
| 62 | } |
|---|
| 63 | |
|---|
| 64 | @misc{GCC2012, |
|---|
| 65 | title = {GNU Compiler Collection 4.7.0}, |
|---|
| 66 | howpublished = {\url{http://gcc.gnu.org/}}, |
|---|
| 67 | year = {2012} |
|---|
| 68 | } |
|---|
| 69 | |
|---|
| 70 | @article {Leroy2009, |
|---|
| 71 | author = {Leroy, Xavier}, |
|---|
| 72 | affiliation = {INRIA Paris-Rocquencourt B.P. 105 78153 Le Chesnay France}, |
|---|
| 73 | title = {A Formally Verified Compiler Back-end}, |
|---|
| 74 | journal = {Journal of Automated Reasoning}, |
|---|
| 75 | publisher = {Springer Netherlands}, |
|---|
| 76 | issn = {0168-7433}, |
|---|
| 77 | keyword = {Computer Science}, |
|---|
| 78 | pages = {363-446}, |
|---|
| 79 | volume = {43}, |
|---|
| 80 | issue = {4}, |
|---|
| 81 | url = {http://dx.doi.org/10.1007/s10817-009-9155-4}, |
|---|
| 82 | note = {10.1007/s10817-009-9155-4}, |
|---|
| 83 | year = {2009} |
|---|
| 84 | } |
|---|
| 85 | |
|---|
| 86 | @book {Moore1996, |
|---|
| 87 | author = {J Strother Moore}, |
|---|
| 88 | title = {Piton: A mechanically verified assembly language}, |
|---|
| 89 | series = {Automated Reasoning Series}, |
|---|
| 90 | volume = {3}, |
|---|
| 91 | isbn = {978-0-7923-3920-5}, |
|---|
| 92 | publisher = {Springer}, |
|---|
| 93 | year = {1996} |
|---|
| 94 | } |
|---|
| 95 | |
|---|
