| 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 |
|---|
| 96 | t 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 | } |
|---|
