1 |
1 @InProceedings{CoquandSiles12, |
|
2 author = {T.~Coquand and V.~Siles}, |
|
3 title = {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory}, |
|
4 booktitle = {Proc.~of the 1st Conference on Certified Programs and Proofs}, |
|
5 pages = {119--134}, |
|
6 year = {2011}, |
|
7 volume = {7086}, |
|
8 series = {LNCS} |
|
9 } |
|
10 |
|
11 @InProceedings{Asperti12, |
|
12 author = {A.~Asperti}, |
|
13 title = {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence}, |
|
14 booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving}, |
|
15 pages = {283--298}, |
|
16 year = {2012}, |
|
17 volume = {7406}, |
|
18 series = {LNCS} |
|
19 } |
|
20 |
|
21 @InProceedings{LammichTuerk12, |
|
22 author = {P.~Lammich and T.~Tuerk}, |
|
23 title = {{A}pplying {D}ata {R}efinement for {M}onadic {P}rograms to {H}opcroft's {A}lgorithm}, |
|
24 booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving}, |
|
25 year = {2012}, |
|
26 volume = {7406}, |
|
27 series = {LNCS}, |
|
28 pages = {166--182} |
|
29 } |
2 |
30 |
3 @PhdThesis{Braibant12, |
31 @PhdThesis{Braibant12, |
4 author = {T.~Braibant}, |
32 author = {T.~Braibant}, |
5 title = {{K}leene {A}lgebras, {R}ewriting {M}odulo {AC}, and {C}ircuits in {C}oq}, |
33 title = {{K}leene {A}lgebras, {R}ewriting {M}odulo {AC}, and {C}ircuits in {C}oq}, |
6 school = {University of Grenoble}, |
34 school = {University of Grenoble}, |
118 pages = {173--190} |
146 pages = {173--190} |
119 } |
147 } |
120 |
148 |
121 |
149 |
122 |
150 |
123 @Unpublished{KraussNipkow11, |
151 @article{KraussNipkow11, |
124 author = {A.~Krauss and T.~Nipkow}, |
152 author = {A.~Krauss and T.~Nipkow}, |
125 title = {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra}, |
153 title = {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra}, |
126 note = {To appear in the Journal of Automated Reasoning}, |
154 journal = {Journal of Automated Reasoning}, |
127 year = {2012} |
155 volume = 49, |
|
156 number = {1}, |
|
157 year = {2012}, |
|
158 pages = {95--106} |
128 } |
159 } |
129 |
160 |
130 @Book{Kozen97, |
161 @Book{Kozen97, |
131 author = {D.~Kozen}, |
162 author = {D.~Kozen}, |
132 title = {{A}utomata and {C}omputability}, |
163 title = {{A}utomata and {C}omputability}, |