cs0603117/a.bbl
1: \newcommand{\noopsort}[1]{}
2: \begin{thebibliography}{}
3: 
4: \bibitem[Bauer et~al., 2002]{BauerEscardoSimpson02}
5: Bauer, A., Escard{\'o}, M., and Simpson, A. (2002).
6: \newblock Comparing functional paradigms for exact real-number computation.
7: \newblock In {\em Automata, languages and programming}, volume 2380 of {\em
8:   Lecture Notes in Comput. Sci.}, pages 489--500. Springer.
9: 
10: \bibitem[Bertot, 2005]{bertot05a}
11: Bertot, Y. (2005).
12: \newblock Filters on coinductive streams, an application to eratosthenes'
13:   sieve.
14: \newblock In Urzyczyn, P., editor, {\em Typed Lambda Calculi and Applications,
15:   TLCA 2005}, pages 102--115. Springer-Verlag.
16: 
17: \bibitem[Bertot and Cast{\'e}ran, 2004]{coqart}
18: Bertot, Y. and Cast{\'e}ran, P. (2004).
19: \newblock {\em Interactive Theorem Proving and Program Development, Coq'Art:the
20:   Calculus of Inductive Constructions}.
21: \newblock Springer-Verlag.
22: 
23: \bibitem[Boehm et~al., 1986]{DBLP:conf/lfp/BoehmCRO86}
24: Boehm, H.-J., Cartwright, R., Riggle, M., and O'Donnell, M.~J. (1986).
25: \newblock Exact real arithmetic: A case study in higher order programming.
26: \newblock In {\em LISP and Functional Programming}, pages 162--173.
27: 
28: \bibitem[Boldo, 2004]{Boldo04}
29: Boldo, S. (2004).
30: \newblock {\em Preuves formelles en arithm{\'e}tiques {\`a}virgule flottante}.
31: \newblock PhD thesis, {\'E}cole Normale Sup'erieure de Lyon.
32: 
33: \bibitem[Boldo et~al., 2002]{BolDauMorThe02}
34: Boldo, S., Daumas, M., Moreau-Finot, C., and Th{\'e}ry, L. (2002).
35: \newblock Computer validated proofs of a toolset for adaptable arithmetic.
36: \newblock {\em Journal of the ACM}.
37: \newblock Submitted.
38: 
39: \bibitem[Boutin, 1997]{Boutin97b}
40: Boutin, S. (1997).
41: \newblock Using reflection to build efficient and certified decision
42:   procedures.
43: \newblock In Abadi, M. and Ito, T., editors, {\em TACS'97}, volume 1281. LNCS,
44:   Springer-Verlag.
45: 
46: \bibitem[Ciaffaglione and di~Gianantonio, 2000]{ciaffaglione.00}
47: Ciaffaglione, A. and di~Gianantonio, P. (2000).
48: \newblock A coinductive approach to real numbers.
49: \newblock In Coquand, T., Dybjer, P., Nordstr\"om, B., and Smith, J., editors,
50:   {\em Types 1999 Workshop, L\"okeberg, Sweden}, number 1956 in LNCS, pages
51:   114--130. Springer-Verlag.
52: 
53: \bibitem[Coquand, 1993]{CoquandInfinite93}
54: Coquand, T. (1993).
55: \newblock Infinite objects in {T}ype {T}heory.
56: \newblock In Barendregt, H. and Nipkow, T., editors, {\em Types for Proofs and
57:   Programs}, volume 806 of {\em LNCS}, pages 62--78. Springer Verlag.
58: 
59: \bibitem[Cruz-Filipe et~al., 2004]{DBLP:conf/mkm/Cruz-FilipeGW04}
60: Cruz-Filipe, L., Geuvers, H., and Wiedijk, F. (2004).
61: \newblock C-corn, the constructive coq repository at nijmegen.
62: \newblock In Asperti, A., Bancerek, G., and Trybulec, A., editors, {\em MKM},
63:   volume 3119 of {\em Lecture Notes in Computer Science}, pages 88--103.
64:   Springer.
65: 
66: \bibitem[Daumas et~al., 2001]{DauRidThe01}
67: Daumas, M., Rideau, L., and Th{\'e}ry, L. (2001).
68: \newblock A generic library of floating-point numbers and its application to
69:   exact computing.
70: \newblock In Boulton, R.~J. and Jackson, P.~B., editors, {\em Theorem Proving
71:   in Higher Order Logics: 14th International Conference, TPHOLs 2001}, volume
72:   2152 of {\em Lecture Notes in Computer Science}, pages 169--184.
73:   Springer-Verlag.
74: 
75: \bibitem[Delahaye and Mayero, 2001]{del.may.2001}
76: Delahaye, D. and Mayero, M. (2001).
77: \newblock Field: une proc\'edure de d\'ecision pour les nombres r\'eels en coq.
78: \newblock In {\em Proceedings of JFLA'2001}. INRIA.
79: 
80: \bibitem[di~Gianantonio, 1996]{diGianantonioGolden96}
81: di~Gianantonio, P. (1996).
82: \newblock A golden ration notation for the real numbers.
83: \newblock Technical Report CS-R9602, CWI, Amsterdam.
84: 
85: \bibitem[di~Gianantonio and Miculan, 2003]{diGianantonioMiculan}
86: di~Gianantonio, P. and Miculan, M. (2003).
87: \newblock A unifying approach to recursive and co-recursive definitions.
88: \newblock In Geuvers, H. and Wiedijk, F., editors, {\em Types for Proofs and
89:   Programs}, volume 2646 of {\em LNCS}, pages 148--161. Springer Verlag.
90: 
91: \bibitem[Dowek et~al., 1993]{coq}
92: Dowek, G., Felty, A., Herbelin, H., Huet, G., Murthy, C., Parent, C.,
93:   Paulin-Mohring, C., and Werner, B. (1993).
94: \newblock {\em The Coq Proof Assistant User's Guide}.
95: \newblock INRIA.
96: \newblock Version 5.8.
97: 
98: \bibitem[Edalat and Potts, 1998]{edalat.98}
99: Edalat, A. and Potts, P.~J. (1998).
100: \newblock A new representation for exact real numbers.
101: \newblock In Brookes, S. and Mislove, M., editors, {\em Electronic Notes in
102:   Theoretical Computer Science}, volume~6. Elsevier Science Publishers.
103: 
104: \bibitem[Gibbons, 2004]{DBLP:conf/mpc/Gibbons04}
105: Gibbons, J. (2004).
106: \newblock Streaming representation-changers.
107: \newblock In Kozen, D. and Shankland, C., editors, {\em MPC}, volume 3125 of
108:   {\em Lecture Notes in Computer Science}, pages 142--168. Springer.
109: 
110: \bibitem[Gim{\'e}nez, 1994]{Gimenez94}
111: Gim{\'e}nez, E. (1994).
112: \newblock Codifying guarded definitions with recursive schemes.
113: \newblock In Dybjer, P., Nordstr{\"o}m, B., and Smith, J., editors, {\em Types
114:   for proofs and Programs}, volume 996 of {\em LNCS}, pages 39--59. Springer
115:   Verlag.
116: 
117: \bibitem[Gosper, 1972]{gosper.72}
118: Gosper, R.~W. (1972).
119: \newblock {HAKMEM}, {I}tem 101 {B}.
120: \newblock \url{http://www.inwap.com/pdp10/hbaker/hakmem/cf.html#item101b}.
121: \newblock MIT AI Laboratory Memo No.239.
122: 
123: \bibitem[Grubba et~al., 2005]{DBLP:conf/cca/2005}
124: Grubba, T., Hertling, P., Tsuiki, H., and Weihrauch, K., editors (2005).
125: \newblock {\em CCA 2005 - Second International Conference on Computability and
126:   Complexity in Analysis, August 25-29, 2005, Kyoto, Japan}, volume 326-7/2005
127:   of {\em Informatik Berichte}. FernUniversit{\"a}t Hagen, Germany.
128: 
129: \bibitem[Hales, 2004]{hales-flyspeck}
130: Hales, T. (2004).
131: \newblock The flyspeck project fact sheet.
132: \newblock \\http://www.math.pitt.edu/\~{}thales/flyspeck/index.html.
133: 
134: \bibitem[Hales, 2000]{Hales00}
135: Hales, T.~C. (2000).
136: \newblock Cannonballs and honeycombs.
137: \newblock {\em Notices of the AMS}, 47(4):440--449.
138: 
139: \bibitem[Hanrot et~al., 2000]{MPFR}
140: Hanrot, G., Lef{\`e}vre, V., P{\'e}lissier, P., and Zimmermann, P. (2000).
141: \newblock The mpfr library.
142: \newblock available at {\tt http://www.mpfr.org}.
143: 
144: \bibitem[Harrison, 1996]{HOL-light}
145: Harrison, J. (1996).
146: \newblock Hol light: A tutorial introduction.
147: \newblock In Srivas, M.~K. and Camilleri, A.~J., editors, {\em FMCAD}, volume
148:   1166 of {\em Lecture Notes in Computer Science}, pages 265--269. Springer.
149: 
150: \bibitem[Harrison, 1998]{HarrisonThesis}
151: Harrison, J. (1998).
152: \newblock {\em Theorem Proving with the Real Numbers}.
153: \newblock Springer-Verlag.
154: 
155: \bibitem[Harrison, 2000]{tphols2000-Harrison}
156: Harrison, J. (2000).
157: \newblock Formal verification of {IA-64} division algorithms.
158: \newblock In Harrison, J. and Aagaard, M., editors, {\em Theorem Proving in
159:   Higher Order Logics: 13th International Conference, TPHOLs 2000}, volume 1869
160:   of {\em Lecture Notes in Computer Science}, pages 234--251. Springer-Verlag.
161: 
162: \bibitem[IEEE, 1987]{IEEE754}
163: IEEE (1987).
164: \newblock {IEEE} standard for binary floating-point arithmetic.
165: \newblock {\em SIGPLAN Notices}, 22(2):9--25.
166: 
167: \bibitem[Lambov, 2005]{DBLP:conf/cca/Lambov05}
168: Lambov, B. (2005).
169: \newblock Reallib: an efficient implementation of exact real arithmetic.
170: \newblock In \cite{DBLP:conf/cca/2005}, pages 169--175.
171: 
172: \bibitem[Mahboubi, 2006]{Mahboubi06}
173: Mahboubi, A. (2006).
174: \newblock Programming and certifying the {CAD} algorithm inside the {Coq}
175:   system.
176: \newblock {\em Mathematical Structures in Computer Science}, this issue.
177: 
178: \bibitem[Mahboubi and Pottier, 2002]{MahboubiPottier2002}
179: Mahboubi, A. and Pottier, L. (2002).
180: \newblock Élimination des quantificateurs sur les réels en {C}oq.
181: \newblock In {\em {J}ourn\'ees {F}rancophones des {L}angages {A}pplicatifs,
182:   Anglet}.
183: 
184: \bibitem[Mayero, 2001]{mayero-thesis}
185: Mayero, M. (2001).
186: \newblock {\em Formalisation et automatisation de preuves en analyses r\'eelle
187:   et num\'erique}.
188: \newblock PhD thesis, Universit\'e Paris VI.
189: 
190: \bibitem[McLaughlin and Harrison, 2005]{mclaughlin-harrison}
191: McLaughlin, S. and Harrison, J. (2005).
192: \newblock A proof-producing decision procedure for real arithmetic.
193: \newblock In Nieuwenhuis, R., editor, {\em CADE-20: 20th International
194:   Conference on Automated Deduction, proceedings}, volume 3632 of {\em Lecture
195:   Notes in Computer Science}, pages 295--314, Tallinn, Estonia.
196:   Springer-Verlag.
197: 
198: \bibitem[M\'enissier-Morain, 1994]{menissier.94}
199: M\'enissier-Morain, V. (1994).
200: \newblock {\em Arithm\'etique exacte, conception, algorithmique et performances
201:   d'une impl\'ementation informatique en pr\'ecision arbitraire}.
202: \newblock Th\`ese, Universit\'e Paris 7.
203: 
204: \bibitem[M{\'e}nissier-Morain, 1995]{MenissierReals95}
205: M{\'e}nissier-Morain, V. (1995).
206: \newblock Conception et algorithmique d'une repr{\'e}sentation
207:   d'arithm{\'e}tique r{\'e}elle en pr{\'e}cision arbitraire.
208: \newblock In {\em Proceedings of the first conference on real numbers and
209:   computers}.
210: 
211: \bibitem[Muller, 1997]{JMMuller}
212: Muller, J.-M. (1997).
213: \newblock {\em Elementary Functions, Algorithms and implementation}.
214: \newblock Birkhauser.
215: 
216: \bibitem[M{\"u}ller, 2005]{DBLP:conf/cca/Muller05}
217: M{\"u}ller, N.~T. (2005).
218: \newblock Implementing exact real numbers efficiently.
219: \newblock In \cite{DBLP:conf/cca/2005}, page 378.
220: 
221: \bibitem[Niqui, 2004]{NiquiThesis}
222: Niqui, M. (2004).
223: \newblock {\em Formalising Exact Arithmetic, Representations, Algorithms, and
224:   Proofs}.
225: \newblock PhD thesis, University of Nijmegen.
226: \newblock ISBN 90-9018333-7.
227: 
228: \bibitem[Nordstr\"{o}m, 1988]{nordstrom88}
229: Nordstr\"{o}m, B. (1988).
230: \newblock Terminating general recursion.
231: \newblock {\em BIT}, 28:605--619.
232: 
233: \bibitem[Paulin-Mohring, 1993]{moh93}
234: Paulin-Mohring, C. (1993).
235: \newblock {Inductive Definitions in the System {Coq} - Rules and Properties}.
236: \newblock In Bezem, M. and Groote, J.-F., editors, {\em Proceedings of the
237:   conference Typed Lambda Calculi and Applications}, number 664 in Lecture
238:   Notes in Computer Science.
239: \newblock LIP research report 92-49.
240: 
241: \bibitem[Russinoff, 1999]{Russinoff99}
242: Russinoff, D.~M. (1999).
243: \newblock {A} {M}echanically {C}hecked {P}roof of {IEEE} {C}ompliance of the
244:   {AMD} {K5} {F}loating-{P}oint {S}quare {R}oot {M}icrocode.
245: \newblock {\em Formal Methods in System Design}, 14(1):75--125.
246: 
247: \bibitem[Vuillemin, 1990]{vuillemin.90}
248: Vuillemin, J.~E. (1990).
249: \newblock Exact real computer arithmetic with continued fractions.
250: \newblock {\em IEEE Transactions on Computers}, 39(8):1087--1105.
251: 
252: \end{thebibliography}
253: