source: Papers/jar-assembler-2015/boender-jar-2015.bib @ 3633

Last change on this file since 3633 was 3555, checked in by mulligan, 5 years ago

dominic, jaap taking another look at the paper

File size: 3.3 KB
Line 
1@article
2{ asperti:user:2007,
3  author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli},
4  title = {User interaction with the {Matita} proof assistant},
5  journal = {Automated Reasoning},
6  pages = {109--139},
7  volume = {39},
8  issue = {2},
9  year = {2007}
10}
11
12@article
13{ sacerdoti-coen:tinycals:2007,
14  author = {Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli},
15  title = {{Tinycals}: Step by Step Tacticals},
16  journal = {Electronic Notes in Theoretical Computer Science},
17  volume = {174},
18  number = {2},
19  pages = {125--142},
20  doi = {http://dx.doi.org/10.1016/j.entcs.2006.09.026},
21  year = {2007}
22}
23
24@incollection
25{ sozeau:subset:2007,
26  author = {Matthieu Sozeau},
27  title = {Subset Coercions in {Coq}},
28  booktitle = {Types for Proofs and Programs},
29  volume = {4502},
30  series = {Lecture Notes in Computer Science},
31  doi = {10.1007/978-3-540-74464-1_16},
32  pages = {237--252},
33  year = {2007}
34}
35
36@inproceedings
37{ asperti:higher-order:2007,
38  author = {Andrea Asperti and Enrico Tassi},
39  title = {Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case},
40  booktitle = {Towards Mechanized Mathematical Assistants: Calculemus},
41  pages = {146--160},
42  series = {Lecture Notes in Computer Science},
43  volume = {4573},
44  year = 2007
45}
46
47@inproceedings
48{ bove:brief:2009,
49  author = {Ana Bove and Peter Dybjer and Ulf Norell},
50  title = {A Brief Overview of {Agda} --- A Functional Language with Dependent Types},
51  booktitle = {Theorem Proving in Higher-order Logics {(TPHOLs)}},
52  year = {2009}
53}
54
55@manual
56{ coq:2004,
57  title = {The {Coq} proof assistant reference manual},
58  author =  {{The Coq development team}},
59  organization = {{LogiCal Project}},
60  note = {Version 8.0},
61  year = {2004},
62  url = {http://coq.inria.fr}
63}
64
65@misc
66{ cerco:2011,
67  title = {The {CerCo} {FET-Open} project},
68  howpublished = {\url{http://cerco.cs.unibo.it/}},
69  year = {2011},
70  key = {CerCo:2011}
71}
72
73@article{Szymanski1978,
74 author = {Szymanski, Thomas G.},
75 title = {Assembling code for machines with span-dependent instructions},
76 journal = {Commun. ACM},
77 issue_date = {April 1978},
78 volume = {21},
79 number = {4},
80 month = apr,
81 year = {1978},
82 issn = {0001-0782},
83 pages = {300--308},
84 numpages = {9},
85 url = {http://doi.acm.org/10.1145/359460.359474},
86 doi = {10.1145/359460.359474},
87 acmid = {359474},
88 publisher = {ACM},
89 address = {New York, NY, USA},
90 keywords = {NP-complete, assemblers, code generation, compilers, computational complexity, span-dependent instructions, variable-length addressing},
91} 
92
93@article{Robertson1979,
94 author = {Robertson, Edward L.},
95 title = {Code Generation and Storage Allocation for Machines with Span-Dependen
96t Instructions},
97 journal = {ACM Trans. Program. Lang. Syst.},
98 issue_date = {July 1979},
99 volume = {1},
100 number = {1},
101 month = jan,
102 year = {1979},
103 issn = {0164-0925},
104 pages = {71--83},
105 numpages = {13},
106 url = {http://doi.acm.org/10.1145/357062.357067},
107 doi = {10.1145/357062.357067},
108 acmid = {357067},
109 publisher = {ACM},
110 address = {New York, NY, USA},
111} 
112
113@article{Dickson2008,
114  author    = {Neil G. Dickson},
115  title     = {A Simple, Linear-Time Algorithm for x86 Jump Encoding},
116  journal   = {CoRR},
117  volume    = {abs/0812.4973},
118  year      = {2008},
119  ee        = {http://arxiv.org/abs/0812.4973},
120  bibsource = {DBLP, http://dblp.uni-trier.de}
121}
Note: See TracBrowser for help on using the repository browser.