Luminy 2004

Calcul formel, algorithmes certifiés, preuves constructives

Meeting held in the Centre International de Rencontre Mathématiques de Luminy, 12-16th January, 2004.

Organisation


This meeting is the continuation of the seminar "Verification and constructive algebra" held in Dagstuhl from 6 to 10 january 2003.

The goal of the meeting is to bring together people from the communities of formal proofs, constructive mathematics and computer algebra (in a wide meaning).

One objective of the meeting is to bridge the gap between conceptual (abstract) and computational (constructive) mathematics, by providing a computational understanding of abstract mathematics.

It is becoming clear that many parts of abstract mathematics can be made constructive and even computational and that abstract mathematics techniques contains an underlying constructive content.

We are not only interested in algorithms however, but also in formal proofs of the correctness of these algorithms.

Computer algebra provides a variety of interesting basic algorithms, from exact linear algebra to various aspects of elimination and real root counting, which are the foundations for much more sophisticated results like nullstellensatz, quantifier elimination etc... It is remarkable that in constructive and computer algebra, progress in sophisticated algorithms often implies progress on basics.

Moreover the scope of computer algebra is now widened by the consideration of seminumerical algorithms. When such algorithms are correctly controlled, they actually deal with real and complex numbers in the constructive meaning of these objects. So computer algebra is lead to fill many objectives of computational analysis.

Providing formal proofs of correctness to the computer algebra community is very useful, specially for algorithms which are basic and used everywhere.

On the other hand, a collection of mathematically non trivial examples is very useful for the formal proof community, which needs also powerful automatic methods from computer algebra.

We observe that the Dagstuhl seminar 03021/1, which seems to have been the first meeting devoted to the topic, was a success and has been very satisfactory for the participants. They decided to create a group under the acronym

"Mathematics, Algorithms, Proofs"

and asked us to organize a similar meeting on january 2004.

List of participants

Here is the list of participants.

Clemens BALLARIN, TU Muenchen
Boltzmannstr. 3, 85748 Garching, GERMANY
ballarin@in.tum.de

STEFANO BERARDI, Turin University
Computer Science Dept. Corso Svizzera 185, 10149 Torino, ITALY
stefano@di.unito.it

Ulrich BERGER, Univ. of Wales
Dept. of computer Science Sigleton Park, SA2 8PP Swansea, ROYAUME-UNI
u.berger@swan.ac.uk

Sylvie BOLDO, ENS Lyon
LIP 46 allée d'Italie, 69364 Lyon CEDEX 07, FRANCE
Sylvie.Boldo@ens-lyon.fr

Wieb BOSMA, Universiteit Nijmegen
Mathematisch Instituut Postbus 9010, 6500 GL Nijmegen, NETHERLANDS (THE)
bosma@math.kun.nl

Stephane CHRETIEN, Univ. Franche-Comté
16 route de Gray, 25030 Besancon, FRANCE
chretien@math.univ-fcomte.fr

Thierry COQUAND, Chalmers University
Computer Science Department, S 41296 Goteborg, SUEDE
coquand@cs.chalmers.se

Fredrik DAHLGREN, Uppsala University
Dept. Math., Lagerhyddsvagen 2,PO Box 480, 75106 Uppsala, SWEDEN
Fredrik.Dahlgren@math.uu.se

Gilles DOWEK, Ecole polytechnique et INRIA
LIX, 91128 Palaiseau Cedex, FRANCE
Gilles.Dowek@polytechnique.fr

Dominique DUVAL, Univ. Joseph Fourier
IMAG - LMCB.P. 53, 38041 Grenoble cedex 9, FRANCE
Dominique.Duval@imag.fr

Silvia GEBELLATO, Muenchen University
Matematisches Institut München Theresienstr. 39, D-80333 München, GERMANY
silvia@math.unipd.it

Herman GEUVERS, Univ. of Nijmegen
Computer Science Toernooiveld, 6500 ED Nijmegen, NETHERLANDS (THE)
herman@cs.kun.nl

Dima GRIGORIEV, Univ. de Rennes
IRMAR, Beaulieu, 35042 Rennes, FRANCE
dima@math.univ-rennes1.fr

ALAIN JACQUEMARD, Univ. Bourgogne
Inst.Math.Bourgogne UFR Sc et Techniques 9 Av. Savary BP 47870, 21078 Dijon, FRANCE
jacmar@u-bourgogne.fr

Yann KIEFFER, IMAG Grenoble
INPG - laboratoire Leibniz 46, avenue Felix Viallet, 38031 Grenoble, FRANCE
Yann.Kieffer@imag.fr

Henri LOMBARDI, Univ. de Franche-Comté
Dept de MathUFR Sciences et Techniques Route de Gray, 25030 Besancon (Cedex), FRANCE
henri.lombardi@univ-fcomte.fr

Assia MAHBOUBI, INRIA Sophia Antipolis
2004, route des Lucioles-BP 93, 06902 Sophia Antipolis (Cedex), FRANCE
assia.mahboubi@inria.fr

Guillaume MELQUIOND, ENS Lyon
Lip 46 allée d'Italie, 69364 Lyon cedex 07, FRANCE
guillaume.melquiond@ens-lyon.fr

Valérie MÉNISSIER-MORAIN, Univ.Paris 6
6, rue du Capitaine Scott, 75015 Paris, FRANCE
Valerie.Menissier-Morain@lip6.fr

Bernard MOURRAIN, INRIA Sophia Antipolis
BP 93, 06902 Sophia Antipolis, FRANCE
mourrain@sophia.inria.fr

Milad NIQUI, University of Nijmegen
Department of Computer Science, P.O.box 9010, NL-6500 Nijmegen, NETHERLANDS (THE)
milad@cs.kun.nl

Steven OBUA, TU Muenchen
Matematisches Institut Boltzmannstr. 3, 85748 Garching, GERMANY
obua@in.tum.de

Paulo OLIVA, BRICS - Basic Research in CS
Ny Munkegade, building 540 , 8000 Aarhus C, DENMARK
pbo@brics.dk

Peter PAULE, RISC University Linz
J. Kepler Altenbergerstrasse 69, A-4040 Linz, AUSTRIA
Peter.Paule@risc.uni-linz.ac.at

Hervé PERDRY, Universidad de cantabria
av de los Castros s/n, 39071 Santander, ESPAGNE
herve.perdry@unican.es

Richard POLLACK, New York University
Courant Institute251 Mercer Street, 10012 New York, U.S.A.
pollack@courant.nyu.edu

Loïc POTTIER, INRIA Sophia
2004 route des lucioles, 06 Sophia Antipolis, FRANCE
Loic.Pottier@sophia.inria.fr

Guénaël RENAULT, Univ. Paris 6
Lip6, 8 rue du capitaine Scott, 75015 Paris, FRANCE
renault@calfor.lip6.fr

Renaud RIOBOO, Univ. Paris 6
Lip6 8 rue du capitaine scott, 75015 Paris, FRANCE
Renaud.Rioboo@lip6.fr

Marie-Francoise ROY, Univ. Rennes 1
IRMAR Campus de Beaulieu, 35042 Rennes CEDEX, FRANCE
marie-francoise.roy@univ-rennes1.fr

Olivier RUATTA, INRIA Sophia
2004 route des Lucioles BP 93, 06902 Sophia Antipolis, FRANCE
oruatta@sophia.inria.fr

Julio RUBIO, Universidad de La Rioja, Spain
Edificio Vives.Calle Luis de Ulloa s/n, 26004 Logroño, ESPAGNE
julio.rubio@dmc.unirioja.es

Giovanni SAMBIN, Univ. di Padova
Dipartimento di Matematica, Via Belzoni 7, 35131 Padova, ITALIE
sambin@math.unipd.it

Carsten SCHNEIDER, University Linz
J.Kepler RISC Altenberger Str. 69, 4040 Linz, AUSTRIA
carsten.schneider@risc.uni-linz.ac.at

Peter SCHUSTER, Universitaet Muenchen
Mathematisches Institut Theresienstr. 39 , 80333 Muenchen, GERMANY
Peter.Schuster@mathematik.uni-muenchen.de

Helmut SCHWICHTENBERG, Universitaet Muenchen
Mathematisches Institut Theresienstr. 39, D-80333 Muenchen, GERMANY
schwicht@mathematik.uni-muenchen.de

Francis SERGERAERT, Univ. Grenoble I
BP 74, 38402 St Martin d'Hères Cedex, FRANCE
Francis.Sergeraert@ujf-grenoble.fr

Bas SPITTERS, University of Nijmegen
Department of Computer Science,P.O.box 9010, NL-6500G Nijmegen, NETHERLANDS (THE)
spitters@cs.kun.nl

Giorgio TRENTINAGLIA, Dipartimento di Matematica, Un
Via Belzoni 7, 35131 Padova, ITALY
gtrentin@math.unipd.it

Ihsen YENGUI, Fac.Sciences. Sfax
Département de Math, 3018 Sfax, TUNISIE
ihsen_yengui@yahoo.fr

Abstracts of the talks

Convenient Reasoning about Substructures — Towards Instantiation of Locales

[slides]

Locales provide means to manage hierarchical specifications in the Isabelle theorem prover, together with contexts of facts (that is, consequences derived from the specifications). Currently, locales only support reasoning in contexts where locale specifications are directly present — for example, if the context includes the specification "group" then all facts about groups are visible. If the context contains a specification importing another specification, then the latter facts are also available in the context — for example, a context including the specification "commutative group" contains all facts about both groups and commutative groups, provided "commutative groups" imports "groups".

Facts are not available in contexts where specifications are not explicitly included, even if the specification is a consequence of other specifications or assumptions present in that context. Facts are neither available in a context containing an object that happens to meet a specification. Of course, it is possible, after showing that an object meets a specification, to instantiate facts manually. However, since specifications are hierarchic, this may involve additional reasoning, which is both tedious and clutters up proof scripts. We discuss an extention to locales that makes this instantiation automatic and easy to use. The extension is intended to make reasoning about subgroups in Isabelle as elegant as many informal proofs by exploiting that subgroups form a lattice.

Stefano BERARDI

An intuitionistic model of Arithmetical Maps

[slides]

We propose a purely intuitionistic equational model $N*$ of arithmetical maps on integers. $N*$ is an informative model: if $\exists x.P(x)$ is true in $N*$, we may intuitionistically deduce $P(n)$ for some integer $n$. There is an universal arrow $Ext: \rightarrow N*$. As a consequence, integers are a dense subset $N$ of $N*$: if a property of the structure $N*$ is true for all $x \in N$, then it is true for all $x \in N$. $N*$ is not obtained through Non-counterexample interpretation, nor through any existing proof-theoretical technique: instead of translating classical proofs into intuitionistic ones, we define a model directly validating Excluded Middle over one-quantifier formulas.

We had several motivations in introducing $N*$:

Ulrich BERGER

A computational interpretation of classical analysis

We study the proof-theoretic and computational properties of the principle of open induction, a reformulation of Nash-Williams' minimal-bad-sequence argument. It is well-know that open induction is classically equivalent to (countable) dependent choice. We show that intuitonistically, the two principles are quite different: Unlike dependent choice, open induction is closed under negative- and A-translation, and hence proves the same Pi02-formulas in classical or intuitionistic arithmetic. We also give a modified realizability interpretation of open induction and obtain in this way a method for extracting programs from classical proofs of Pi02-formulas using open induction (or dependent choice). The computational interpretations of classical countable choice and classical dependent choice derived from our method are essentially the same as the interpretations given by Berardi, Bezem and Coquand and provide a new proof-theoretic explanation of their results.

Sylvie BOLDO

Formal proofs about computer arithmetic: some faithful results

[slides]

I will present our latest results about polynomial evaluation in order to compute elementary functions. Common knowledge is that Horner's rule is a good scheme unless the indeterminate is close to one of the polynomial's roots. We propose here criteria for one step of Horner's scheme to be faithful. All the results were formally checked with our Coq floating-point formalization. I will then present some perspectives and debatable questions : how to complete our implementation into the IEEE-754 standard (exceptions, traps, vectors of bits...) ? How to handle other systems ?

Thierry COQUAND

Dynamical Methods in Algebra

[slides]

The notion of dynamical proofs [2] leads to constructive versions of some classical abstract algebraic results whose proofs involve Zorn's lemma. This approach allows to reason constructively about structures that often can be shown -not- to exist effectively, like the algebraic closure of an arbitrary field. I will try to survey this approach, explaining the connections and differences with Kronecker's approach to algebra. There are also strong connections with point-free topology [1] (for the description, for instance of the Zariski spectrum), with geometric logic, but also with the method D5 [3] introduced in computer algebra.

[1] Th. Coquand, Th., H. Persson. Valuations and Dedekind's Prague theorem. J. Pure Appl. Algebra 155 (2001), 121--129.

[2] M. Coste, H. Lombardi, M.F. Roy. Dynamical method in algebra: effective Nullstellensätze. (English. English summary) Ann. Pure Appl. Logic 111 (2001), 203--256.

[3] J. Della Dora, C. Dicrescenzo, D. Duval, About a new method for computing in algebraic number fields, in: B.F. Caviness (Ed.), EUROCAL '85, Lecture Notes in Computer Science, vol. 204, Springer, 1985, 289--290.

Gilles DOWEK

Confluence as a cut elimination property (invited talk)

[slides]

The goal of this talk is to compare two notions, one coming from the theory of rewrite systems and the other from proof theory: confluence and cut elimination. We show that to each rewrite system on terms, we can associate a logical system: asymmetric deduction modulo this rewrite system and that the confluence property of the rewrite system is equivalent to the cut elimination property of the associated logical system. This equivalence, however, does not extend to rewrite systems directly rewriting atomic propositions.

Dominique DUVAL

Diagrammatic specifications

[slides]

Diagrammatic specifications are defined and several examples are presented, including overloaded specifications.

Silvia GEBELLATO

The basic picture as invariance under transfer along a relation

(joint work with G. Sambin)

The basic picture is the theory originated from basic pairs, that is binary relations between two sets, and from relation-pairs, that is commutative squares with a notion of equality. It started a new constructive approach to topology based on symmetry between pointwise and pointfree notions, and logical duality between open and closed subsets.

In this talk an abstract characterization of the basic picture will be presented, which let us to describe the pointfree notions of open and closed subsets as the outcome of transferring the structure of the category of subsets along a (continuous) relation.

The starting point which made this characterization possible was the systematic use of a new relation between subsets, besides inclusion, which expresses the fact that two subsets have a common element abstractly and in a positive way. This relation, introduced by G. Sambin, has been called "overlap".

By means of overlap, a structural method characterizing relations between sets has been developed and enabled us to describe the basic picture as a structure invariant under continuous relations.

Herman GEUVERS

CCoRN, the Constructive Coq Repository at Nijmegen

At Nijmegen we have created a repository of formalised constructive mathematics in the proof assistant Coq. This grew out of a constructive formalization of the Fundamental Theorem of Algebra (FTA), where a lot of basic algebra and analysis was alraedy formalized. The goal of CCoRN (and also the FTA formalization) is not so much to prove impressive mathematical theorems but to create a basis repository of formalized mathematics in which people can prove their own (impressive) mathematical theorems.

Important issues are: documentation, notation and automation. In the talk I will describe the contents of CCoRN, its (short) history and the guidelines that we (try to) keep for our developments. Furthermore I will speak about the (possible) (dis)advantages of working constructively and the "missing parts" of CCoRN.

Dima GRIGORIEV

Factoring and solving linear partial differential equations

The problem of factoring a linear partial differential operator is studied. An algorithm is designed which allows one to factor an operator when its symbol is separable, and if in addition the operator has enough right factors then it is completely reducible. Since finding the space of solutions of a completely reducible operator reduces to the same for its right factors, we apply this approach and execute a complete analysis of factoring and solving a second-order operator in two independent variables. Some results on factoring third-order operators are exhibited.

Assia MAHBOUBI

Induction over real numbers

[slides]

We have a constructive look at a quite elementary lemma of standard real analysis which can be considered as an « open induction principle ». Following an idea of Th. Coquand, who has prouved the result for the dyadic Cantor set, we provide a new constructive proof also using monotone bar induction. This latter proof works directly with the real numbers and an appropriate kind of real open sets. The computational content of such an induction principle over real numbers is quite easy to extract but it would be rather interesting to understand its status in the hierarchy of non-classical axioms.

Milad NIQUI

Exact Real Arithmetic using Coinductive Types

The aim of this talk is to show the relationship between admissibility (a topological property) of real number representations, and productivity (a type theoretic property) of the algorithms for exact real arithmetic. In order to show this relationship we discuss the Potts' approach to exact real arithmetic which is based on a normalisation algorithm on a coinductive type of expression trees. We consider formalisation of these notions in type theory and we discuss how changes in representation for real numbers can affect the coinductive nature of the proofs in type theory.

Steven OBUA

Towards a Machine-Checked Proof of the Kepler Conjecture

The Kepler Conjecture was proven in 1998 by Thomas Hales. The Flyspeck project is about formalizing his proof. First an overview is given over what the Kepler Conjecture is all about, and for a better understanding its analogy in two dimensions is discussed. Then the proof given by Thomas Hales will be sketched. Then some of the first steps taken in the Flyspeck project are outlined.

Paulo OLIVA

Bounded Functional Interpretation

[slides]

In this talk I will present a version of Goedel's functional interpretation which is insensitive to bounded quantifiers. The interpretation makes fundamental use of the majorizability relation (due to Howard/Bezem) in order to extend the notion of "bound" to all finite types. I will first present the original motivation for the work and the basic framework for defining the interpretation. In the second part of the talk, we shall see applications of the interpretation to (classical) proofs which involve ineffective principles such as weak Koenig's lemma. All the results in the talk were obtained in collaboration with Professor Fernando Ferreira, from Lisbon University.

Peter PAULE

Computer-Assisted Proving and Finding in Combinatorics and Special Functions (invited talk)

I start with supplementing the MAP-club manifesto by a picture of Buchberger's creativity spiral describing the process of mathematical discovery. The talk discusses concrete examples where an interplay of algorithmic experimental mathematics and the activity of proving has led to the discovery of new theorems. The examples are taken from partition analysis, a computational method created by MacMahon for combinatorial problem solving about hundred years ago. In a research project joint with G.E. Andrews (PennState) and A. Riese (RISC-Linz) MacMahon's method has been translated into a computer algebra algorithm. Applications range from finding nonnegative integer solutions of linear systems of Diophantine inequalities and equations, to computing generating functions for number partitions defined over various posets.

Hervé PERDRY

Strongly Noetherian rings and Lasker-Noether rings

[slides]

We give a new constructive definition for Noetherian rings. It has a very concrete statement and is nevertheless strong enough to prove constructively the termination of algorithms involving "trees of ideals".

The efficiency of such algorithms (at least for providing clear and intuitive constructive proofs) is illustrated by a constructive approach to classical topics from ideal theory: we give constructive proofs for the existence of the minimal primes over an ideal, of its radical (intersection of finitely many primes), of its primary decomposition, in a wide class of polynomial rings, the Lasker-Noether rings.

Loic POTTIER

Quotients in type theory

Renaud RIOBOO

The Foc distribution

[slides]

This talk presents the basics of the next release of the FoC distribution. After a recall of the FoC programming language and its concepts, we present some tools that enable a FoC programmer to document hist code. In the same spirit than JavaDoc or Doxygen structured comments are added by the programmer in order to have them included in the documentation. FoCDoC has the advantage over existing tools for other programming languages that rendering is achieved using the MathML W3C norm and is viewable by most of the recent Web browsers.

Julio RUBIO

Emulating proof-by-hand with Isabelle

[slides]

In the talk, we will report on the state of a project devoted to give a mechanised proof of the Basic Perturbation Lemma (or BPL, in short). The BPL is a central result in algorithmic homological algebra, and has been intensively used in the development of the Kenzo system (a Common Lisp program designed by Sergeraert for computations in Algebraic Topology). Thus, to get a mechanised proof of the BPL seems a necessary step towards certified versions of the algorithms appearing in Kenzo.

We will argue that to reach this objective, it is convenient to emulate in a proof assistant (Isabelle, in our case) the very essence of a concrete proof-by-hand. We illustrate the role of abstraction in mechanised reasoning (not so different from its use in other computer-based mathematics, as symbolic computation), by means of simple examples. The abstraction level is constrained by contextual knowledge, in our case by the need of having computational content in the proof objects.

Then, these general ideas are particularised to a specific lemma in the proof of the BPL.

Giovanni SAMBIN

Putting predicative topology in algebraic terms

An intuitionistic and predicative approach to topology has pulled out a whole structure which I have called the Basic Picture. It is based on symmetries and logical dualities, and gives both usual and pointfree (or formal) topology as a special case, when a notion of convergence is added. The main novelty with respect to standard topology is the use of mathematical notions corresponding to existential statements.

In this talk I will introduce the notion of S-algebra, a natural algebraic axiomatization of the notion of powerset in which the notion of overlap of two subsets ("there exists a point belonging to both subsets") is taken as primitive. By suppressing overlap, one gets back the notion of complete Heyting algebra, or frame. The additional expressive power provided by overlap is considerable: I will show that the language of S-algebras is strong enough to be able to develop the whole basic picture and formal topology in algebraic terms. Thus S-algebras appear as the correct algebraic structures to deal abstractly with the computational contents of topology.

Carsten SCHNEIDER

Proving and Finding Multisum Identities in Difference Fields

[slides]

Sigma is a summation package, implemented in the computer algebra system Mathematica, that enables to discover and prove nested multisum identities. Based on Karr's difference field theory (1981) this package allows to find all solutions of parameterized linear difference equations in a very general difference field setting, so called Pi-Sigma-fields. Starting from these summation algorithms I will present a more general framework that enables to deal with summation problems which involve objects that can be described by a linear recurrence, like orthogonal polynomials.

All these aspects will be illustrated by proving the celebrated Totally Symmetric Plane Partition Theorem (Stembridge, 1995) with computer algebra methods. Special emphasize is put on the verification of these proofs.

Peter SCHUSTER

Why Formal Geometry, and How? (invited talk)

Formal geometry is abstract algebraic geometry done in an elementary point-free way inspired by formal topology. Every move is avoided that would affect any computational information contained in the initial data. We try to give a flavour of the tentative practice.

Helmut SCHWICHTENBERG

Program Extraction in Constructive Analysis

[slides]

We are interested in exact real numbers, as opposed to floating point numbers. The final goal is to develop the basics of real analysis in such a way that from a proof of an existence formula one can extract a program. For instance, from a proof of the intermediate value theorem we want to extract a program that, given an arbitrary error bound 2-k, computes a rational x where the given function is zero up to the error bound. - The novel aspect of the present work is the development of elementary constructive analysis in such a way that witnesses have as low a type level as possible. This clearly is important for the complexity of the extracted programs.

Francis SERGERAERT

The status of Postnikov invariants in algebraic topology

[slides]

The computability problem about the Postnikov complexes is solved and the next natural computability problem in algebraic topology, the isomorphism problem between two Postnikov towers, once translated into the standard algebraic framework, leads to an algebraic decision problem which has its own interest, the nature of which being arithmetical. Because of the negative answer by Matiyasevich to Hilbert's tenth problem, maybe we are in front of a new surprising kind of incompleteness in Algebraic Topology. The talk is devoted to a description as simple as possible of this situation, to explain how the statement of the correspondant algebraic problem is obtained. We thus obtain a general decision problem in arithmetic, the solution of which is crucial in simply connected algebraic topology.

More generally the computability status of the Postnikov towers is really fantastic. The definition of a Postnikov tower contains in particular some "invariants''; it is explained in the talk why this terminology is erroneous: the nature of an equality relation is misunderstood. Transforming these pseudo-invariants into correct invariants is the computability problem we are interested in; because of Matiyasevich, it is even not clear a positive solution of this problem exists.

Bas SPITTERS

Constructive Algebraic Integration Theory without Choice

In this talk I'll present a constructive development of integration algebras in the sense of Segal. Using point-free topology, a Stone representation theorem for these algebras will be obtained and applied to the group algebra of a compact group. Thus we obtain a point-free description of the space of characters. Using countable choice and a positivity predicate we can then construct all the characters. In this way we obtain an elementary and apparently new proof of the Peter-Weyl theorem. It appears that this is the first *mathematical* application of a positivity predicate.

Finally, we compare this approach to Richman's choice-free constructive mathematics using Brouwer's spreads.

[Joint work with Thierry Coquand]

Ihsen YENGUI

A constructive deciphering of a Suslin's lemma

In this talk I'll explain how to decipher constructively the Suslin's proof of a Lemma which played a central role in the resolution of Serre's conjecture.

This lemma says that for a commutative ring ${\bf A}$ if the ideal $(v_1(X),\ldots,v_n(X))$ equals ${\bf A}[X]$ where $v_1$ is monic and $n \geq 3$, then there exist $\Gamma_1,\ldots,\Gamma_{\ell} \in {\rm E}_{n-1}({\bf A}[X])$ such that

\begin{displaymath}({\rm Res}(v_1, e_1.\Gamma_1 \,^t{ (v_2,\ldots,v_n)},\ldots, ... ... Res} (v_1, e_1.\Gamma_{\ell} \,^t{ (v_2,\ldots,v_n)} = {\bf A}\end{displaymath}


The constructive proof we give may be a model for miming constructively abstract proofs in which one works modulo each maximal ideal to prove that a given ideal contains 1.

Luminy 2004 · Schedule

Here is the final schedule.

Monday

9h00-10h00 SERGERAERT Francis The status of Postnikov invariants in algebraic topology
10h30-11h30 BALLARIN Clemens Algebraic substructures in Isabelle.
11h30-12h30 RUBIO Julio Emulating proof-by-hand with Isabelle
14h30-15h30 COQUAND Thierry Dynamical Methods in Algebra
16h00-17h00 PERDRY Herve Strongly Noetherian rings and Lasker-Noether rings
17h00-18h0 YENGUI Ihsen A constructive deciphering of a lemma of Suslin

Tuesday

9h00-10h00 DOWEK Gilles Confluence as a cut elimination property (invited talk)
10h30-11h30 SCHWICHTENBERG Helmut Program Extraction in Constructive Analysis
11h30-12h30 GRIGORIEV Dima Weak Bézout inequality for D-modules
14h30-15h30 BOLDO Sylvie Formal proofs about computer arithmetic: some faithful results
16h00-17h00 RIOBOO Renaud The Foc distribution
17h00-18h00 NIQUI Milad Exact Real Arithmetic using Coinductive Types

Wednesday

9h00-10h00 PAULE Peter Computer-Assisted Proving and Finding in Combinatorics and Special Functions (invited talk)
10h30-11h30 MAHBOUBI Assia Induction over real numbers
11h30-12h30 DUVAL Dominique Diagrammatic specifications

Thursday

9h00-10h00 SCHUSTER Peter Why Formal Geometry and How? (invited talk)
10h30-11h30 OLIVA Paulo Bounded functional interpretation
11h30-12h30 BERARDI Stefano An intuitionistic model of Arithmetical Maps
14h30-15h30 POTTIER Loïc Quotients in type theory
16h00-17h00 OBUA Steven Towards a Machine-Checked Proof of the Kepler Conjecture
17h00-18h00 GEBELLATO Silvia The basic picture as invariance under transfer along a relation

Friday

9h00-10h00 SAMBIN Giovani Putting predicative topology in algebraic terms
10h30-11h30 SPITTERS Bas Constructive Algebraic Integration Theory without Choice
11h30-12h30 BERGER Ulrich A computation interpretation of classical analysis
14h30-15h30 GEUVERS Herman CCoRN, the Constructive Coq Repository at Nijmegen
16h00-17h00 SCHNEIDER Carsten Proving and Finding Multisum Identities in Difference Fields