Previous | 
Home
Section: Overall Objectives
Highlights of the Year
This year, we complete a first work emblematic of the
interdisciplinary activity of the team: a computer-algebra based
formal proof of irrationality of the mathematical constant
Research Program
Application Domains
New Results
- Creative telescoping for bivariate hyperexponential functions
- Creative telescoping for rational functions
- Complexity of the uncoupling of linear functional systems
- Computation of integrals related to the Ising model
- Non-D-finite excursions in the quarter plane
- A human proof of Gessel's lattice path conjecture
- Efficient algorithms for rational first integrals
- Reactive document checking in Coq
- Efficient normalization of ring/field expressions in Coq
- Documentation of Coq's canonical structures
- Maintenance and development of the SSReflect extension for Coq and its user manual
- Efficient proof-search techniques in sequent calculus
- A formal proof of the irrationality
of
- Documentation of the Mathematical Components libraries
Bilateral Contracts and Grants with Industry
Partnerships and Cooperations
Bibliography
Research Program
Application Domains
New Results
- Creative telescoping for bivariate hyperexponential functions
- Creative telescoping for rational functions
- Complexity of the uncoupling of linear functional systems
- Computation of integrals related to the Ising model
- Non-D-finite excursions in the quarter plane
- A human proof of Gessel's lattice path conjecture
- Efficient algorithms for rational first integrals
- Reactive document checking in Coq
- Efficient normalization of ring/field expressions in Coq
- Documentation of Coq's canonical structures
- Maintenance and development of the SSReflect extension for Coq and its user manual
- Efficient proof-search techniques in sequent calculus
- A formal proof of the irrationality
of
- Documentation of the Mathematical Components libraries
Bilateral Contracts and Grants with Industry
Partnerships and Cooperations
Bibliography