Bibliography

Publications of the year

Doctoral Dissertations and Habilitation Theses

1B. Morcrette.

Combinatoire analytique et modèles d'urnes, Université Pierre et Marie Curie - Paris VI, June 2013, version du 25 Juin 2013.

http://hal.inria.fr/tel-00843046

Articles in International Peer-Reviewed Journals

2A. Bostan, S. Boukraa, G. Christol, S. Hassani, J.-M. Maillard.

Ising n-fold integrals as diagonals of rational functions and integrality of series expansions, in: Journal of Physics A: Mathematical and Theoretical, April 2013, vol. 46, pp. 185202-185245. [ DOI : 10.1088/1751-8113/46/18/185202 ]

http://hal.inria.fr/hal-00780422
3A. Bostan, K. Raschel, B. Salvy.

Non-D-finite excursions in the quarter plane, in: Journal of Combinatorial Theory, Series A, October 2013, vol. 121, pp. 45-63. [ DOI : 10.1016/j.jcta.2013.09.005 ]

http://hal.inria.fr/hal-00697386
4P. Dumas.

Joint Spectral Radius, Dilation Equations, and Asymptotic Behavior of Radix-Rational Sequences, in: Linear Algebra and its Applications, March 2013, vol. 438, n^o 5, pp. 2107-2126. [ DOI : 10.1016/j.laa.2012.10.013 ]

http://hal.inria.fr/hal-00780568

Invited Conferences

5A. Mahboubi.

The Rooster and the Butterflies, in: CICM 2013 - Conference on Intelligent Computer Mathematics - 2013, Bath, United Kingdom, J. Carette, D. Aspinal, C. Lange, P. Sojka, W. Windsteiger (editors), Lecture Notes in Artificial Intelligence, Springer, July 2013, vol. 7961, pp. 1-18. [ DOI : 10.1007/978-3-642-39320-4_1 ]

http://hal.inria.fr/hal-00825074
6A. Mahboubi, E. Tassi.

Canonical Structures for the working Coq user, in: ITP 2013, 4th Conference on Interactive Theorem Proving, Rennes, France, S. Blazy, C. Paulin, D. Pichardie (editors), LNCS, Springer, 2013, vol. 7998, pp. 19-34. [ DOI : 10.1007/978-3-642-39634-2_5 ]

http://hal.inria.fr/hal-00816703

International Conferences with Proceedings

7B. Barras, L. D. C. Gonzalez Huesca, H. Herbelin, Y. Régis-Gianas, E. Tassi, M. Wenzel, B. Wolff.

Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems, in: MKM/Calculemus/DML, Bath, United Kingdom, 2013, pp. 359-363.

http://hal.inria.fr/hal-00908980
8A. Bostan, S. Chen, F. Chyzak, Z. Li, G. Xin.

Hermite Reduction and Creative Telescoping for Hyperexponential Functions, in: ISSAC'13 - 38th International Symposium on Symbolic and Algebraic Computation, Boston, United States, Northeastern University, Boston, Massachusetts, USA, 2013, pp. 77-84. [ DOI : 10.1145/2465506.2465946 ]

http://hal.inria.fr/hal-00780067
9A. Bostan, F. Chyzak, É. De Panafieu.

Complexity Estimates for Two Uncoupling Algorithms, in: ISSAC'13 - 38th International Symposium on Symbolic and Algebraic Computation, Boston, United States, Northeastern University, Boston, Massachusetts, USA, 2013, pp. 85-92. [ DOI : 10.1145/2465506.2465941 ]

http://hal.inria.fr/hal-00780010
10A. Bostan, P. Lairez, B. Salvy.

Creative telescoping for rational functions using the Griffiths-Dwork method, in: ISSAC'13 - 38th International Symposium on Symbolic and Algebraic Computation, Boston, United States, Northeastern University, Boston, Massachusetts, USA, 2013, pp. 93-100. [ DOI : 10.1145/2465506.2465935 ]

http://hal.inria.fr/hal-00777675
11M. Farooque, S. Lengrand, A. Mahboubi.

A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus, in: LFMTP - International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice - 2013, Boston, United States, A. Momigliano, B. Pientka, R. Pollack (editors), ACM, September 2013. [ DOI : 10.1145/2503887.2503892 ]

http://hal.inria.fr/hal-00854426
12G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen, F. Garillot, S. Le Roux, A. Mahboubi, R. O'Connor, S. Ould Biha, I. Pasca, L. Rideau, A. Solovyev, E. Tassi, L. Théry.

A Machine-Checked Proof of the Odd Order Theorem, in: ITP 2013, 4th Conference on Interactive Theorem Proving, Rennes, France, S. Blazy, C. Paulin, D. Pichardie (editors), LNCS, Springer, 2013, vol. 7998, pp. 163-179. [ DOI : 10.1007/978-3-642-39634-2_14 ]

http://hal.inria.fr/hal-00816699

Scientific Books (or Scientific Book chapters)

13P. Aczel, B. Ahrens, T. Altenkirch, S. Awodey, B. Barras, A. Bauer, Y. Bertot, M. Bezem, T. Coquand, E. Finster, D. Grayson, H. Herbelin, A. Joyal, D. Licata, P. Lumsdaine, A. Mahboubi, P. Martin-Löf, S. Melikhov, A. Pelayo, A. Polonsky, M. Shulman, M. Sozeau, B. Spitters, B. Van Den Berg, V. Voevodsky, M. Warren, C. Angiuli, A. Bordg, G. Brunerie, C. Kapulkin, E. Rijke, K. Sojakova, J. Avigad, C. Cohen, R. Constable, P.-L. Curien, P. Dybjer, M. Escardó, K.-B. Hou, N. Gambino, R. Garner, G. Gonthier, T. Hales, R. Harper, M. Hofmann, P. Hofstra, J. Koch, N. Kraus, N. Li, Z. Luo, M. Nahas, E. Palmgren, E. Riehl, D. Scott, P. Scott, S. Soloviev.

Homotopy Type Theory: Univalent Foundations of Mathematics, Aucun, 2013, 448 p.

http://hal.inria.fr/hal-00935057

Other Publications

14A. Bostan, G. Chèze, T. Cluzeau, J.-A. Weil.

Efficient Algorithms for Computing Rational First Integrals and Darboux Polynomials of Planar Polynomial Vector Fields, October 2013.

http://hal.inria.fr/hal-00871663
15A. Bostan, I. Kurkova, K. Raschel.

A human proof of Gessel's lattice path conjecture, 2013, 23 pages, 3 figures.

http://hal.inria.fr/hal-00858083
16P. Dumas.

Rational series and asymptotic expansion for linear homogeneous divide-and-conquer recurrences, 2013.

http://hal.inria.fr/hal-00840659

References in notes

17M. Abramowitz, I. A. Stegun (editors)

Handbook of mathematical functions with formulas, graphs, and mathematical tables, Dover, New York, 1992, xiv+1046 p, Reprint of the 1972 edition.
18Computer Algebra Errors, Article in mathematics blog MathOverflow.

http://mathoverflow.net/questions/11517/computer-algebra-errors
19F. W. J. Olver, D. W. Lozier, R. F. Boisvert, C. W. Clark (editors)

NIST Handbook of mathematical functions, Cambridge University Press, 2010.
20M. Armand, B. Grégoire, A. Spiwack, L. Théry.

Extending Coq with Imperative Features and its Application to SAT Verication, in: Interactive Theorem Proving, international Conference, ITP 2010, Edinburgh, Scotland, July 11–14, 2010, Proceedings, Lecture Notes in Computer Science, Springer, 2010.
21B. Beckermann, G. Labahn.

A uniform approach for the fast computation of matrix-type Padé approximants, in: SIAM J. Matrix Anal. Appl., 1994, vol. 15, n^o 3, pp. 804–823.
22A. Benoit, F. Chyzak, A. Darrasse, S. Gerhold, M. Mezzarobba, B. Salvy.

The Dynamic Dictionary of Mathematical Functions (DDMF), in: The Third International Congress on Mathematical Software (ICMS 2010), K. Fukuda, J. van der Hoeven, M. Joswig, N. Takayama (editors), Lecture Notes in Computer Science, 2010, vol. 6327, pp. 35–41.

http://dx.doi.org/10.1007/978-3-642-15582-6_7
23M. Boespflug, M. Dénès, B. Grégoire.

Full reduction at full throttle, in: First International Conference on Certified Programs and Proofs, Taiwan, December 7–9, Lecture Notes in Computer Science, Springer, 2011.
24S. Boldo, C. Lelay, G. Melquiond.

Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives, in: Certified Programs and Proofs, C. Hawblitzel, D. Miller (editors), Lecture Notes in Computer Science, Springer Berlin Heidelberg, 2012, vol. 7679, pp. 289-304.

http://dx.doi.org/10.1007/978-3-642-35308-6_22
25S. Boldo, G. Melquiond.

Flocq: A Unified Library for Proving Floating-point Algorithms in Coq, in: Proceedings of the 20th IEEE Symposium on Computer Arithmetic, Tübingen, Germany, July 2011, pp. 243–252.
26A. Bostan.

Algorithmes rapides pour les polynômes, séries formelles et matrices, in: Actes des Journées Nationales de Calcul Formel, Luminy, France, 2010, pp. 75–262, Les cours du CIRM, tome 1, numéro 2.

http://ccirm.cedram.org:80/ccirm-bin/fitem?id=CCIRM_2010__1_2_75_0
27A. Bostan, S. Boukraa, S. Hassani, J.-M. Maillard, J.-A. Weil, N. Zenine.

Globally nilpotent differential operators and the square Ising model, in: J. Phys. A: Math. Theor., 2009, vol. 42, n^o 12, 50 p.

http://dx.doi.org/10.1088/1751-8113/42/12/125206
28A. Bostan, S. Chen, F. Chyzak, Z. Li.

Complexity of creative telescoping for bivariate rational functions, in: ISSAC'10: Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation, New York, NY, USA, ACM, 2010, pp. 203–210.

http://doi.acm.org/10.1145/1837934.1837975
29A. Bostan, F. Chyzak, G. Lecerf, B. Salvy, É. Schost.

Differential equations for algebraic functions, in: ISSAC'07: Proceedings of the 2007 international symposium on Symbolic and algebraic computation, C. W. Brown (editor), ACM Press, 2007, pp. 25–32.

http://dx.doi.org/10.1145/1277548.1277553
30A. Bostan, F. Chyzak, M. van Hoeij, L. Pech.

Explicit formula for the generating series of diagonal 3D rook paths, in: Sém. Loth. Comb., 2011, vol. B66a, 27 p.

http://www.emis.de/journals/SLC/wpapers/s66bochhope.html
31A. Bostan, M. Kauers.

The complete generating function for Gessel walks is algebraic, in: Proceedings of the American Mathematical Society, September 2010, vol. 138, n^o 9, pp. 3063–3078, With an appendix by Mark van Hoeij.
32F. Chyzak.

An extension of Zeilberger's fast algorithm to general holonomic functions, in: Discrete Math., 2000, vol. 217, n^o 1-3, pp. 115–134, Formal power series and algebraic combinatorics (Vienna, 1997).
33F. Chyzak, M. Kauers, B. Salvy.

A Non-Holonomic Systems Approach to Special Function Identities, in: ISSAC'09: Proceedings of the Twenty-Second International Symposium on Symbolic and Algebraic Computation, J. May (editor), 2009, pp. 111–118.

http://dx.doi.org/10.1145/1576702.1576720
34F. Chyzak, B. Salvy.

Non-commutative elimination in Ore algebras proves multivariate identities, in: J. Symbolic Comput., 1998, vol. 26, n^o 2, pp. 187–227.
35T. Coquand, G. P. Huet.

The Calculus of Constructions, in: Inf. Comput., 1988, vol. 76, n^o 2/3, pp. 95-120.

http://dx.doi.org/10.1016/0890-5401(88)90005-3
36T. Coquand, C. Paulin-Mohring.

Inductively defined types, in: Proceedings of Colog'88, P. Martin-Löf, G. Mints (editors), Lecture Notes in Computer Science, Springer-Verlag, 1990, vol. 417.
37D. Delahaye, M. Mayero.

Dealing with algebraic expressions over a field in Coq using Maple, in: J. Symbolic Comput., 2005, vol. 39, n^o 5, pp. 569–592, Special issue on the integration of automated reasoning and computer algebra systems.

http://dx.doi.org/10.1016/j.jsc.2004.12.004
38F. Garillot, G. Gonthier, A. Mahboubi, L. Rideau.

Packaging Mathematical Structures, in: Theorem Proving in Higher-Order Logics, S. Berghofer, T. Nipkow, C. Urban, M. Wenzel (editors), Lecture Notes in Computer Science, Springer, 2009, vol. 5674, pp. 327–342.
39J. von zur. Gathen, J. Gerhard.

Modern computer algebra, 2nd, Cambridge University Press, New York, 2003, xiv+785 p.
40G. Gonthier.

Formal proofs—the four-colour theorem, in: Notices of the AMS, 2008, vol. 55, n^o 11, pp. 1382-1393.
41G. Gonthier, A. Mahboubi.

An introduction to small scale reflection in Coq, in: Journal of Formalized Reasoning, 2010, vol. 3, n^o 2, pp. 95–152.
42G. Gonthier, A. Mahboubi, E. Tassi.

A Small Scale Reflection Extension for the Coq system, Inria, 2008, n^o RR-6455.

http://hal.inria.fr/inria-00258384
43G. Gonthier, E. Tassi.

A language of patterns for subterm selection, in: ITP, LNCS, 2012, vol. 7406, pp. 361–376.
44B. Grégoire, A. Mahboubi.

Proving Equalities in a Commutative Ring Done Right in Coq, in: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, Lecture Notes in Computer Science, Springer, 2005, vol. 3603, pp. 98–113.
45T. Hales.

Formal proof, in: Notices of the AMS, 2008, vol. 55, n^o 11, pp. 1370-1380.
46J. Harrison.

A HOL Theory of Euclidean space, in: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, J. Hurd, T. Melham (editors), Lecture Notes in Computer Science, Springer-Verlag, 2005, vol. 3603.
47J. Harrison.

Formalizing an analytic proof of the prime number theorem, in: Journal of Automated Reasoning, 2009, vol. 43, pp. 243–261, Dedicated to Mike Gordon on the occasion of his 60th birthday.
48J. Harrison.

Theorem proving with the real numbers, CPHC/BCS distinguished dissertations, Springer, 1998, I p.
49J. Harrison.

A Machine-Checked Theory of Floating Point Arithmetic, in: Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs'99, Nice, France, Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, L. Théry (editors), Lecture Notes in Computer Science, Springer-Verlag, 1999, vol. 1690, pp. 113–130.
50J. Harrison, L. Théry.

A Skeptic's Approach to Combining HOL and Maple, in: J. Autom. Reason., December 1998, vol. 21, n^o 3, pp. 279–294.

http://dx.doi.org/10.1023/A:1006023127567
51F. Johansson.

Another Mathematica bug, Article on personal blog.

http://fredrik-j.blogspot.fr/2009/07/another-mathematica-bug.html
52C. Koutschan.

A fast approach to creative telescoping, in: Math. Comput. Sci., 2010, vol. 4, n^o 2-3, pp. 259–266.

http://dx.doi.org/10.1007/s11786-010-0055-0
53A. Mahboubi.

Implementing the cylindrical algebraic decomposition within the Coq system, in: Mathematical Structures in Computer Science, 2007, vol. 17, n^o 1, pp. 99–127.
54R. Matuszewski, P. Rudnicki.

Mizar: the first 30 years, in: Mechanized Mathematics and Its Applications, 2005, vol. 4, 2005 p.
55M. Mayero.

Problèmes critiques et preuves formelles, Université Paris 13, novembre 2012, Habilitation à Diriger des Recherches.
56M. Mezzarobba.

NumGfun: a package for numerical and analytic computation and D-finite functions, in: ISSAC 2010—Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation, New York, ACM, 2010, pp. 139–146.

http://dx.doi.org/10.1145/1837934.1837965
57P. Paule, M. Schorn.

A Mathematica version of Zeilberger's algorithm for proving binomial coefficient identities, in: J. Symbolic Comput., 1995, vol. 20, n^o 5-6, pp. 673–698, Symbolic computation in combinatorics $Δ_{1}$ (Ithaca, NY, 1993).

http://dx.doi.org/10.1006/jsco.1995.1071
58B. Petersen.

Maple, Personal web site.

http://people.oregonstate.edu/~peterseb/maple/
59P. Rudnicki, A. Trybulec.

On the Integrity of a Repository of Formalized Mathematics, in: Proceedings of the Second International Conference on Mathematical Knowledge Management, London, UK, MKM '03, Springer-Verlag, 2003, pp. 162–174.

http://dl.acm.org/citation.cfm?id=648071.748518
60B. Salvy, P. Zimmermann.

Gfun: a Maple package for the manipulation of generating and holonomic functions in one variable, in: ACM Trans. Math. Software, 1994, vol. 20, n^o 2, pp. 163–177.
61N. J. A. Sloane, S. Plouffe.

The Encyclopedia of Integer Sequences, Academic Press, San Diego, 1995.
62The Coq Development Team.

The Coq Proof Assistant: Reference Manual.

http://coq.inria.fr/doc/
63The Mathematical Component Team.

A Formalization of the Odd Order Theorem using the Coq proof assistant, September 2012.

http://www.msr-inria.fr/projects/mathematical-components/
64L. Théry.

A Machine-Checked Implementation of Buchberger's Algorithm, in: J. Autom. Reasoning, 2001, vol. 26, n^o 2, pp. 107-137.

http://dx.doi.org/10.1023/A:1026518331905
65K. Wegschaider.

Computer generated proofs of binomial multi-sum identities, RISC, J. Kepler University, May 1997, 99 p.
66S. Wolfram.

Mathematica: A system for doing mathematics by computer (2nd ed.), Addison-Wesley, 1992, I p.
67D. Zeilberger.

Opinion 94: The Human Obsession With “Formal Proofs” is a Waste of the Computer's Time, and, Even More Regretfully, of Humans' Time, 2009.

http://www.math.rutgers.edu/~zeilberg/Opinion94.html
68D. Zeilberger.

A holonomic systems approach to special functions identities, in: J. Comput. Appl. Math., 1990, vol. 32, n^o 3, pp. 321–368.
69D. Zeilberger.

The method of creative telescoping, in: J. Symbolic Comput., 1991, vol. 11, n^o 3, pp. 195–204.

Previous |

Home