Sites Inria

English version

Equipe de recherche SPECFUN

Publications de l'équipe SPECFUN

2019

Article dans une revue

titre
On the least common multiple of several random integers
auteur
Alin Bostan, Alexander Marynych, Kilian Raschel
article
Journal of Number Theory, Elsevier, 2019, 204, pp.113-133. ⟨10.1016/j.jnt.2019.03.017⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01984389/file/1901.03002.pdf BibTex
titre
Formally Verified Approximations of Definite Integrals
auteur
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
article
Journal of Automated Reasoning, Springer Verlag, 2019, 62 (2), pp.281-300. ⟨10.1007/s10817-018-9463-7⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01630143/file/main.pdf BibTex
titre
Rigid continuation paths I. Quasilinear average complexity for solving polynomial systems
auteur
Pierre Lairez
article
Journal of the American Mathematical Society, American Mathematical Society, In press
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01631778/file/rigid-paths-1.pdf BibTex
titre
Subresultants of $(x-\alpha)^m$ and $(x-\beta)^n$, Jacobi polynomials and complexity
auteur
Alin Bostan, T Krick, A Szanto, M Valdettaro
article
Journal of Symbolic Computation, Elsevier, In press, ⟨10.1016/j.jsc.2019.10.003⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01966640/file/BKSV19-arxiv2.pdf BibTex

Communication dans un congrès

titre
Computing the volume of compact semi-algebraic sets
auteur
Pierre Lairez, Marc Mezzarobba, Mohab Safey El Din
article
ISSAC 2019 - International Symposium on Symbolic and Algebraic Computation, Jul 2019, Beijing, China
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-02110556/file/volumes.pdf BibTex
titre
Big Prime Field FFT on Multi-core Processors
auteur
Svyatoslav Covanov, Davood Mohajerani, Marc Moreno Maza, Linxiao Wang
article
ISSAC 2019 - International Symposium on Symbolic and Algebraic Computation, Jul 2019, Pékin, China
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02191652/file/cmmw-2019.ISSAC.sigconf.pdf BibTex

Pré-publication, Document de travail

titre
Explicit degree bounds for right factors of linear differential operators
auteur
Alin Bostan, Tanguy Rivoal, Bruno Salvy
article
2019
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-02154679/file/factorisation.pdf BibTex

2018

Article dans une revue

titre
Computing the Homology of Basic Semialgebraic Sets in Weak Exponential Time
auteur
Peter Bürgisser, Felipe Cucker, Pierre Lairez
article
Journal of the ACM (JACM), Association for Computing Machinery, 2018, 66 (1), pp.1-30. ⟨10.1145/3275242⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01545657/file/Semialgebraic.pdf BibTex
titre
Computing solutions of linear Mahler equations
auteur
Frédéric Chyzak, Thomas Dreyfus, Philippe Dumas, Marc Mezzarobba
article
Mathematics of Computation, American Mathematical Society, 2018, 87, pp.2977-3021. ⟨10.1090/mcom/3359⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01418653/file/mahlersols.pdf BibTex
titre
Counting walks with large steps in an orthant
auteur
Alin Bostan, Mireille Bousquet-Mélou, Stephen Melczer
article
ArXiv e-prints, 2018
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01802706/file/ls.pdf BibTex
titre
Becker's conjecture on Mahler functions
auteur
Jason Bell, Frédéric Chyzak, Michael Coons, Philippe Dumas
article
Transactions of the American Mathematical Society, American Mathematical Society, In press, pp.17
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01885598/file/BellChyzakCoonsDumas-2018-BCM.pdf BibTex

Communication dans un congrès

titre
Fast Coefficient Computation for Algebraic Power Series in Positive Characteristic
auteur
Alin Bostan, Xavier Caruso, Gilles Christol, Philippe Dumas
article
Thirteenth Algorithmic Number Theory Symposium ANTS-XIII, Jul 2018, Madison, United States
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01816375/file/fastNth.pdf BibTex
titre
Generalized Hermite Reduction, Creative Telescoping and Definite Integration of D-Finite Functions
auteur
Alin Bostan, Frédéric Chyzak, Pierre Lairez, Bruno Salvy
article
ISSAC 2018 - International Symposium on Symbolic and Algebraic Computation, Jul 2018, New York, United States. pp.1-8, ⟨10.1145/3208976.3208992⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01788619/file/redct-final.pdf BibTex

Pré-publication, Document de travail

titre
A numerical transcendental method in algebraic geometry
auteur
Pierre Lairez, Emre Can Sertöz
article
2018
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01932147/file/hodge_rank.pdf BibTex
titre
Bijections between Łukasiewicz walks and generalized tandem walks
auteur
Frédéric Chyzak, Karen Yeats
article
2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01891792/file/sixsteps.pdf BibTex

2017

Article dans une revue

titre
Subresultants in multiple roots: an extremal case
auteur
Alin Bostan, Carlos d'Andrea, Teresa Krick, Agnès Szanto, Marcelo Valdettaro
article
Linear Algebra and its Applications, Elsevier, 2017, 529, pp.185-198. ⟨10.1016/j.laa.2017.04.019⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01588546/file/1608.03740.pdf BibTex
titre
On Matrices With Displacement Structure: Generalized Operators and Faster Algorithms
auteur
Alin Bostan, Claude-Pierre Jeannerod, Christophe Mouilleron, Eric Schost
article
SIAM Journal on Matrix Analysis and Applications, Society for Industrial and Applied Mathematics, 2017, 38 (3), pp.733-775. ⟨10.1137/16M1062855⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01588552/file/M106285-final.pdf BibTex
titre
Formal solutions of completely integrable Pfaffian systems with normal crossings
auteur
Moulay A. Barkatou, Maximilian Jaroschek, Suzy Maddah
article
Journal of Symbolic Computation, Elsevier, 2017, 81, pp.41 - 68. ⟨10.1016/j.jsc.2016.11.018⟩
Accès au bibtex
BibTex
titre
Multiple binomial sums
auteur
Alin Bostan, Pierre Lairez, Bruno Salvy
article
Journal of Symbolic Computation, Elsevier, 2017, 80 (2), pp.351--386. ⟨10.1016/j.jsc.2016.04.002⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01220573/file/binomsums.pdf BibTex
titre
Algebraic Diagonals and Walks: Algorithms, Bounds, Complexity
auteur
Alin Bostan, Louis Dumont, Bruno Salvy
article
Journal of Symbolic Computation, Elsevier, 2017, Special issue on the conference ISSAC 2015: Symbolic computation and computer algebra, 83, pp.68-92. ⟨10.1016/j.jsc.2016.11.006 ⟩
Accès au bibtex
https://arxiv.org/pdf/1510.04526 BibTex
titre
Hypergeometric Expressions for Generating Functions of Walks with Small Steps in the Quarter Plane
auteur
Alin Bostan, Frédéric Chyzak, Mark van Hoeij, Manuel Kauers, Lucien Pech
article
European Journal of Combinatorics, Elsevier, 2017, 61, pp.242-275. ⟨10.1016/j.ejc.2016.10.010⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01332175/file/walks.pdf BibTex
titre
A human proof of Gessel's lattice path conjecture
auteur
Alin Bostan, Irina Kurkova, Kilian Raschel
article
Transactions of the American Mathematical Society, American Mathematical Society, 2017, 369 (2, February 2017), pp.1365-1393
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00858083/file/BoKuRa13-rev%5B3%5D.pdf BibTex

HDR

titre
Computer Algebra for Lattice path Combinatorics
auteur
Alin Bostan
article
Symbolic Computation [cs.SC]. Université Paris 13, 2017
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/tel-01660300/file/HDR.pdf BibTex

Autre publication

titre
The Coq Proof Assistant, version 8.7.1
auteur
The Coq Development Team
article
2017, pp.1-571. ⟨10.5281/zenodo.1133970⟩
Accès au bibtex
BibTex

Ouvrage (y compris édition critique et traduction)

titre
Algorithmes Efficaces en Calcul Formel
auteur
Alin Bostan, Frédéric Chyzak, Marc Giusti, Romain Lebreton, Grégoire Lecerf, Bruno Salvy, Eric Schost
article
⟨published by the Authors⟩, 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01431717/file/aecf%40svn1386.pdf BibTex

Pré-publication, Document de travail

titre
Théories géométriques pour l'algèbre des nombres réels
auteur
Henri Lombardi, Assia Mahboubi
article
2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01426164/file/Reels-geom-court.pdf BibTex
titre
Formal Solutions of Singularly Perturbed Linear Differential Systems
auteur
Suzy Maddah, Moulay A. Barkatou
article
2017
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01417265/file/November2016_sys_with_parameters_arxiv.pdf BibTex

2016

Article dans une revue

titre
Computing periods of rational integrals
auteur
Pierre Lairez
article
Mathematics of Computation, American Mathematical Society, 2016, 85, pp.1719-1752. ⟨10.1090/mcom/3054⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00981114/file/arxiv.article.pdf BibTex
titre
On 3-dimensional lattice walks confined to the positive octant
auteur
Alin Bostan, Mireille Bousquet-Mélou, Manuel Kauers, Stephen Melczer
article
Annals of Combinatorics, Springer Verlag, 2016, pp.36. ⟨10.1007/s00026-016-0328-7⟩
Accès au bibtex
https://arxiv.org/pdf/1409.3669 BibTex
titre
Machine-checked mathematics
auteur
Assia Mahboubi
article
Nieuw Archief voor Wiskunde, Richard Boucherie, 2016, 5/17 (3), pp.5
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01363284/file/naw5-2016-17-3-172.pdf BibTex
titre
An Induction Principle over Real Numbers
auteur
Assia Mahboubi
article
Archive for Mathematical Logic, Springer Verlag, 2016, ⟨10.1007/s00153-016-0513-8⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01376054/file/main.pdf BibTex
titre
Efficient Algorithms for Computing Rational First Integrals and Darboux Polynomials of Planar Polynomial Vector Fields
auteur
Alin Bostan, Guillaume Chèze, Thomas Cluzeau, Jacques-Arthur Weil
article
Mathematics of Computation, American Mathematical Society, 2016, 85 (299), pp.1393--1425
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00871663/file/BoChClWe14.pdf BibTex

Communication dans un congrès

titre
Formal Verification of Smart Contracts: Short Paper
auteur
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, Santiago Zanella-Béguelin
article
ACM Workshop on Programming Languages and Analysis for Security, Oct 2016, Vienna, Austria. ⟨10.1145/2993600.2993611⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01400469/file/solidether.pdf BibTex
titre
Formally Verified Approximations of Definite Integrals
auteur
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
article
Interactive Theorem Proving, Aug 2016, Nancy, France. ⟨10.1007/978-3-319-43144-4_17⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01289616/file/main.pdf BibTex
titre
Fast Computation of the $N$th Term of an Algebraic Series over a Finite Prime Field
auteur
Alin Bostan, Gilles Christol, Philippe Dumas
article
ISSAC '16, Jul 2016, Waterloo, Ontario, Canada. ⟨10.1145/2930889.2930904⟩
Accès au bibtex
https://arxiv.org/pdf/1602.00545 BibTex
titre
Computation of the Similarity Class of the $p$-Curvature
auteur
Alin Bostan, Xavier Caruso, Éric Schost
article
ISSAC 2016, Jul 2016, Waterloo, ON, Canada. pp.111-118, ⟨10.1145/2930889.2930897⟩
Accès au bibtex
https://arxiv.org/pdf/1605.06126 BibTex
titre
Efficient Algorithms for Mixed Creative Telescoping
auteur
Alin Bostan, Louis Dumont, Bruno Salvy
article
ISSAC 2016, Jul 2016, Waterloo, Canada. pp.127-134, ⟨10.1145/2930889.2930907⟩
Accès au bibtex
https://arxiv.org/pdf/1605.05082 BibTex

Cours

titre
Algebraicity and transcendence of power series: combinatorial and computational aspects
auteur
Alin Bostan
article
Doctoral. 3rd Algorithmic and Enumerative Combinatorics Summer School, Hagenberg, 2016 Austria. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/cel-01391907/file/aec16-p5.pdf https://hal.inria.fr/cel-01391907/file/aec16-p1.pdf https://hal.inria.fr/cel-01391907/file/aec16-p2.pdf https://hal.inria.fr/cel-01391907/file/aec16-p3.pdf https://hal.inria.fr/cel-01391907/file/aec16-p4.pdf BibTex
titre
Diviser pour régner Algèbre et analyse
auteur
Philippe Dumas
article
Master. Centre International de Rencontres Mathématiques, Marseille, France. 2016, pp.80
Accès au texte intégral et bibtex
https://hal.inria.fr/cel-01388741/file/booklet-alea16-dumas.pdf BibTex

Rapport

titre
A Small Scale Reflection Extension for the Coq system
auteur
Georges Gonthier, Assia Mahboubi, Enrico Tassi
article
[Research Report] RR-6455, Inria Saclay Ile de France. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00258384/file/main.pdf BibTex

2015

Article dans une revue

titre
Diagonals of rational functions and selected differential Galois groups
auteur
A. Bostan, S. Boukraa, J-M. Maillard, Jacques-Arthur Weil
article
Journal of Physics A: Mathematical and Theoretical, IOP Publishing, 2015, Exactly solved models and beyond: a special issue in honour of R J Baxter's 75th birthday, 48 (50), pp.504001-504030. ⟨10.1088/1751-8113/48/50/504001⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01242668/file/1507.03227v2.pdf BibTex
titre
Compter les excursions sur un échiquier
auteur
Alin Bostan, Kilian Raschel
article
Pour la science, Pour la science, 2015, pp.40-46
Accès au bibtex
BibTex

Communication dans un congrès

titre
Axiomatic constraint systems for proof search modulo theories
auteur
Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Jean-Marc Notin, Assia Mahboubi
article
10th International Symposium on Frontiers of Combining Systems (FroCoS'15), Sep 2015, Wroclaw, Poland. ⟨10.1007/978-3-319-24246-0_14⟩
Accès au bibtex
https://arxiv.org/pdf/1412.6790 BibTex
titre
Asynchronous processing of Coq documents: from the kernel up to the user interface
auteur
Bruno Barras, Carst Tankink, Enrico Tassi
article
Proceedings of ITP, Aug 2015, Nanjing, China
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01135919/file/full.pdf BibTex
titre
A Fast Algorithm for Computing the p-Curvature
auteur
Alin Bostan, Xavier Caruso, Éric Schost
article
ISSAC 2015, Jul 2015, Bath, United Kingdom. pp.69-76, ⟨10.1145/2755996.2756674⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01164471/file/BoCaSc15-issac.pdf BibTex
titre
Algebraic Diagonals and Walks
auteur
Alin Bostan, Louis Dumont, Bruno Salvy
article
ISSAC'15 International Symposium on Symbolic and Algebraic Computation, Jul 2015, Bath, United Kingdom. pp.77-84, ⟨10.1145/2755996.2756663⟩
Accès au bibtex
https://arxiv.org/pdf/1510.04080 BibTex

Direction d'ouvrage, Proceedings, Dossier

titre
Nablus2014 CIMPA Summer School
auteur
Pierre Nicodeme, Nicolas Pouyanne, Brigitte Chauvin, Jeremie Lumbroso, Basile Morcrette, Cécile Mailler
article
Pierre Nicodeme. Aug 2014, Nablus, Palestinian Territories. pp.138, 2015, Proceedings of the Nablus2014 CIMPA Summer School
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01214113/file/nablus14proc.pdf BibTex

Cours

titre
Computer Algebra for Lattice Path Combinatorics
auteur
Alin Bostan
article
Doctoral. Ellwangen, Germany. 2015
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/cel-01242698/file/ellwangen15-l1.pdf https://hal.archives-ouvertes.fr/cel-01242698/file/ellwangen15-l2.pdf https://hal.archives-ouvertes.fr/cel-01242698/file/ellwangen15-l3.pdf BibTex

2014

Article dans une revue

titre
Asymptotic expansions for linear homogeneous divide-and-conquer recurrences: Algebraic and analytic approaches collated
auteur
Philippe Dumas
article
Theoretical Computer Science, Elsevier, 2014, 548, pp.25-53. ⟨10.1016/j.tcs.2014.06.036⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01065761/file/Dumas2014.pdf BibTex
titre
Non-D-finite excursions in the quarter plane
auteur
Alin Bostan, Kilian Raschel, Bruno Salvy
article
Journal of Combinatorial Theory, Series A, Elsevier, 2014, 121, pp.45-63. ⟨10.1016/j.jcta.2013.09.005⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00697386/file/BoRaSa12.pdf BibTex
titre
Un ordinateur pour vérifier les preuves mathématiques
auteur
Assia Mahboubi
article
Images des Mathématiques, CNRS, 2014
Accès au bibtex
BibTex
titre
On the existence of telescopers for mixed hypergeometric terms
auteur
Shaoshi Chen, Frédéric Chyzak, Ruyong Feng, Guofeng Fu, Ziming Li
article
Journal of Symbolic Computation, Elsevier, 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00991211/file/criteria.pdf BibTex

Communication dans un congrès

titre
A fast algorithm for computing the characteristic polynomial of the p-curvature
auteur
Alin Bostan, Xavier Caruso, Éric Schost
article
ISSAC - 39th International Symposium on Symbolic and Algebraic Computation, Jul 2014, Kobe, Japan. ⟨10.1145/2608628.2608650⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00994033/file/BoCaSc14.pdf BibTex
titre
Computing necessary integrability conditions for planar parametrized homogeneous potentials
auteur
Alin Bostan, Thierry Combot, Mohab Safey El Din
article
ISSAC'14 - International Symposium on Symbolic and Algebraic Computation, Jul 2014, Kobe, Japan. pp.67-74, ⟨10.1145/2608628.2608662⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00994116/file/BoCoSa14-hal.pdf BibTex
titre
Asynchronous Editing for Coq
auteur
Carst Tankink
article
The Coq Workshop 2014, Jul 2014, Vienna, Austria
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01092008/file/coq-workshop-2014.pdf BibTex
titre
PIDE for Asynchronous Interaction with Coq
auteur
Carst Tankink
article
User Interfaces for Theorem Provers, Jul 2014, Vienna, Austria. pp.73 - 83, ⟨10.4204/EPTCS.167.9⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01091907/file/uitp-2014.pdf BibTex
titre
Computer-checked mathematics: a formal proof of the odd order theorem
auteur
Assia Mahboubi
article
The Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2014, Vienna, Austria. ⟨10.1145/2603088.2603090⟩
Accès au bibtex
BibTex
titre
A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
auteur
Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi
article
ITP - 5th International Conference on Interactive Theorem Proving, 2014, Vienna, Austria
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00984057/file/main.pdf BibTex

HDR

titre
The ABC of Creative Telescoping --- Algorithms, Bounds, Complexity
auteur
Frédéric Chyzak
article
Symbolic Computation [cs.SC]. Ecole Polytechnique X, 2014
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01069831/file/h.pdf BibTex

Rapport

titre
Coq 8.4 Reference Manual
auteur
Pierre Boutillier, Stephane Glondu, Benjamin Grégoire, Hugo Herbelin, Pierre Letouzey, Pierre-Marie Pédrot, Yann Régis-Gianas, Matthieu Sozeau, Arnaud Spiwack, Enrico Tassi
article
[Research Report] Inria. 2014
Accès au bibtex
BibTex

Thèse

titre
Périodes d'intégrales rationnelles : algorithmes et applications
auteur
Pierre Lairez
article
Calcul formel [cs.SC]. École polytechnique, 2014. Français
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/tel-01089130/file/these.pdf BibTex

2013

Article dans une revue

titre
A constructive version of Laplace's proof on the existence of complex roots
auteur
Cyril Cohen, Thierry Coquand
article
Journal of Algebra, Elsevier, 2013, 381, pp.110-115. ⟨10.1016/j.jalgebra.2013.01.016⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00592284/file/laplace1.pdf BibTex
titre
Ising n-fold integrals as diagonals of rational functions and integrality of series expansions
auteur
Alin Bostan, S. Boukraa, G. Christol, S. Hassani, J.-M. Maillard
article
Journal of Physics A: Mathematical and Theoretical, IOP Publishing, 2013, 46, pp.185202-185245. ⟨10.1088/1751-8113/46/18/185202⟩
Accès au bibtex
https://arxiv.org/pdf/1211.6645 BibTex
titre
Joint Spectral Radius, Dilation Equations, and Asymptotic Behavior of Radix-Rational Sequences
auteur
Philippe Dumas
article
Linear Algebra and its Applications, Elsevier, 2013, 438 (5), pp.2107-2126. ⟨10.1016/j.laa.2012.10.013⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00780568/file/LAA-Dumas-vHal.pdf BibTex

Communication dans un congrès

titre
A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus
auteur
Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi
article
LFMTP - International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice - 2013, Sep 2013, Boston, United States. ⟨10.1145/2503887.2503892⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00854426/file/DPLL-LK.pdf BibTex
titre
Creative telescoping for rational functions using the Griffiths-Dwork method
auteur
Alin Bostan, Pierre Lairez, Bruno Salvy
article
ISSAC'13 - 38th International Symposium on Symbolic and Algebraic Computation, Northeastern University, Boston, Massachusetts, USA, Jul 2013, Boston, United States. pp.93-100, ⟨10.1145/2465506.2465935⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00777675/file/arxiv.issac24p-bostan.pdf BibTex
titre
Hermite Reduction and Creative Telescoping for Hyperexponential Functions
auteur
Alin Bostan, Shaoshi Chen, Frédéric Chyzak, Ziming Li, Guoce Xin
article
ISSAC'13 - 38th International Symposium on Symbolic and Algebraic Computation, Northeastern University, Boston, Massachusetts, USA, Jul 2013, Boston, United States. pp.77-84, ⟨10.1145/2465506.2465946⟩
Accès au bibtex
https://arxiv.org/pdf/1301.5038 BibTex
titre
Complexity Estimates for Two Uncoupling Algorithms
auteur
Alin Bostan, Frédéric Chyzak, Élie de Panafieu
article
ISSAC'13 - 38th International Symposium on Symbolic and Algebraic Computation, Northeastern University, Boston, Massachusetts, USA, Jul 2013, Boston, United States. pp.85-92, ⟨10.1145/2465506.2465941⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00780010/file/BoChPa13.pdf BibTex
titre
Canonical Structures for the working Coq user
auteur
Assia Mahboubi, Enrico Tassi
article
ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.19-34, ⟨10.1007/978-3-642-39634-2_5⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00816703/file/main.pdf BibTex
titre
A Machine-Checked Proof of the Odd Order Theorem
auteur
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry
article
ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.163-179, ⟨10.1007/978-3-642-39634-2_14⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00816699/file/main.pdf BibTex
titre
The Rooster and the Butterflies
auteur
Assia Mahboubi
article
CICM 2013 - Conference on Intelligent Computer Mathematics - 2013, Jul 2013, Bath, United Kingdom. pp.1-18, ⟨10.1007/978-3-642-39320-4_1⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00825074/file/main.pdf BibTex
titre
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
auteur
Bruno Barras, Lourdes del Carmen Gonzalez Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
article
MKM/Calculemus/DML, Jul 2013, Bath, United Kingdom. pp.359-363
Accès au bibtex
BibTex

Ouvrage (y compris édition critique et traduction)

titre
Homotopy Type Theory: Univalent Foundations of Mathematics
auteur
Peter Aczel, Benedikt Ahrens, Thorsten Altenkirch, Steve Awodey, Bruno Barras, Andrej Bauer, Yves Bertot, Marc Bezem, Thierry Coquand, Eric Finster, Daniel Grayson, Hugo Herbelin, André Joyal, Dan Licata, Peter Lumsdaine, Assia Mahboubi, Per Martin-Löf, Sergey Melikhov, Alvaro Pelayo, Andrew Polonsky, Michael Shulman, Matthieu Sozeau, Bas Spitters, Benno van den Berg, Vladimir Voevodsky, Michael Warren, Carlo Angiuli, Anthony Bordg, Guillaume Brunerie, Chris Kapulkin, Egbert Rijke, Kristina Sojakova, Jeremy Avigad, Cyril Cohen, Robert Constable, Pierre-Louis Curien, Peter Dybjer, Martín Escardó, Kuen-Bang Hou, Nicola Gambino, Richard Garner, Georges Gonthier, Thomas Hales, Robert Harper, Martin Hofmann, Pieter Hofstra, Joachim Koch, Nicolai Kraus, Nuo Li, Zhaohui Luo, Michael Nahas, Erik Palmgren, Emily Riehl, Dana Scott, Philip Scott, Sergei Soloviev
article
Aucun, pp.448, 2013
Accès au bibtex
BibTex

Thèse

titre
Combinatoire analytique et modèles d'urnes
auteur
Basile Morcrette
article
Combinatoire [math.CO]. Université Pierre et Marie Curie - Paris VI, 2013. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00843046/file/these_web.pdf BibTex

2012

Article dans une revue

titre
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
auteur
Cyril Cohen, Assia Mahboubi
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (1:02), pp.1-40. ⟨10.2168/LMCS-8 (1:02) 2012⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00593738/file/1201.3731.pdf BibTex
titre
A binomial-like matrix equation
auteur
Alin Bostan, Thierry Combot
article
American Mathematical Monthly, Mathematical Association of America, 2012, 119 (7), pp.593-597. ⟨10.4169/amer.math.monthly.119.07.593⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00780438/file/BoCo11.pdf BibTex

Communication dans un congrès

titre
Construction of real algebraic numbers in Coq
auteur
Cyril Cohen
article
ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00671809/file/main.pdf BibTex
titre
Fast Computation of Common Left Multiples of Linear Ordinary Differential Operators
auteur
Alin Bostan, Frédéric Chyzak, Ziming Li, Bruno Salvy
article
ISSAC 2012 - 37th International Symposium on Symbolic and Algebraic Computation, Jul 2012, Grenoble, France. pp.99-106
Accès au bibtex
https://arxiv.org/pdf/1205.0879 BibTex
titre
Power Series Solutions of Singular (q)-Differential Equations
auteur
Alin Bostan, Muhammad F. I. Chowdhury, Romain Lebreton, Bruno Salvy, Éric Schost
article
ISSAC '12: 37th International Symposium on Symbolic and Algebraic Computation, Jul 2012, Grenoble, France. pp.107-114
Accès au bibtex
https://arxiv.org/pdf/1205.3414 BibTex
titre
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
auteur
François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond
article
6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. pp.67-81, ⟨10.1007/978-3-642-31365-3_8⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00687640/file/main.pdf BibTex
titre
Construction des nombres algébriques réels en Coq
auteur
Cyril Cohen
article
JFLA - Journées Francophones des Langages Applicatifs - 2012, Feb 2012, Carnac, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00665965/file/paper_11.pdf BibTex

Document associé à des manifestations scientifiques

titre
Calcul formel pour la combinatoire
auteur
Alin Bostan, Bruno Salvy
article
Journées ALEA 2012, Mar 2012, Luminy, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00780435/file/BostanSalvy_part1.pdf https://hal.inria.fr/hal-00780435/file/BostanSalvy_part2.pdf BibTex

Thèse

titre
Formalized algebraic numbers: construction and first-order theory.
auteur
Cyril Cohen
article
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2012. English
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/pastel-00780446/file/main.pdf BibTex

Pré-publication, Document de travail

titre
Ising n-fold integrals as diagonals of rational functions and integrality of series expansions: integrality versus modularity
auteur
A. Bostan, S. Boukraa, G. Christol, S. Hassani, J. -M. Maillard
article
2012
Accès au bibtex
https://arxiv.org/pdf/1211.6031 BibTex
titre
Simulating the DPLL(T ) procedure in a sequent calculus with focusing
auteur
Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi
article
2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00690392/file/MainHal.pdf BibTex

2011

Article dans une revue

titre
Homotopy techniques for multiplication modulo triangular sets
auteur
Alin Bostan, Muhammad F. I. Chowdhury, Joris van der Hoeven, Éric Schost
article
Journal of Symbolic Computation, Elsevier, 2011, 46 (12), pp.1378-1402. ⟨10.1016/j.jsc.2011.08.015⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00819155/file/BoChHoSc11.pdf BibTex

2009

Ouvrage (y compris édition critique et traduction)

titre
Calcul formel : mode d'emploi. Exemples en Maple
auteur
Philippe Dumas, Claude Gomez, Bruno Salvy, Paul Zimmermann
article
Sans, pp.326, 2009
Accès au bibtex
BibTex

2002

Article dans une revue

titre
Tracking of Objects in Video Scenes with Time Varying Content
auteur
Amal Mahboubi, Jenny Benois-Pineau, Dominique Barba
article
EURASIP Journal on Advances in Signal Processing, SpringerOpen, 2002, EURASIP Journal on Advances in Signal Processing, 2002 (6), pp.582 - 594. ⟨10.1155/S1110865702000902⟩
Accès au bibtex
BibTex

Suivez Inria