MAP =
2014 =20

9:30 - 10:00 | Welcome | |

10:00 - 11:00 | Claire T=C3=AAte |
Invited tutorial: Depth,=20
dimension and resolution in Commutative Algebra |

30min break | ||

11:30 - 12:30 | Alain Herremann |
Invited talk: How=20
to define constructivity? Some few things we can learn from=20
history. |

lunch break (1h45) | ||

14:15 - 15:15 | Claude Quitt=C3=A9 |
Invited talk: Playing=20
with monomials of k[X_1, =E2=80=A6, X_n] |

15:15 - 16:15 | Konstantin Mischaikow |
Invited tutorial: Towards=
=20
an Algebraic Framework for Nonlinear Dynamics |

45min break | ||

17:00 - 18:00 | Timothy Gowers |
External event: Fully=20
automatic problem solving with human-style=20
output. |

9:00 - 10:00 | Claire T=C3=AAte |
Invited tutorial: Depth,=20
dimension and resolution in Commutative Algebra |

10:00 - 10:30 | Francis Sergeraert |
Contributed talk: Spectra=
l=20
Sequences downgraded to elementary Gauss =
Reductions |

30min break | ||

11:00 - 12:00 | Fr=C3=A9d=C3=A9ric Chyzak |
Invited talk: A=20
Computer-Algebra-Based Formal Proof of the Irrationality of=20
=CE=B6(3) |

12:00 - 12:30 | Anders M=C3=B6rtberg and Cyril Cohen |
Contributed talk: Formalizi=
ng=20
elementary divisor rings in Coq |

lunch break (1h45) | ||

14:15 - 15:15 | Noam Zeilberger |
Invited talk: Refinin=
g=20
the meaning of types |

15:15 - 15:45 | Xavier Caruso, David Roe and Tristan =
Vaccon |
Contributed talk: Tracking=20
p-adic precision |

15:45 - 16:15 | MAP meeting | |

Evening | MAP dinner |

9:00 - 10:00 | Konstantin Mischaikow |
Invited tutorial: Towards=
=20
an Algebraic Framework for Nonlinear Dynamics |

10:00 - 10:30 | Marc Giusti and Jean-Claude Yakoubsohn |
Contributed talk: Multipl=
icity=20
hunting and approximating multiple roots of polynomial=20
systems |

30min break | ||

11:00 - 12:00 | Luca Moci |
Invited talk: Matroids=20
over a ring: motivations, examples, =
applications. |

12:00 - 12:30 | Alain Giorgetti, Richard Genestier and Valerio=20
Senni |
Contributed talk: Software=
=20
Engineering and Enumerative Combinatorics |

lunch break (1h45) | ||

14:15 - 15:15 | Christophe Raffalli |
Invited talk: Hilbert's=
=20
17th problem via cut-elimination |

15:15 - 16:15 | Claire T=C3=AAte |
Invited tutorial: Depth,=20
dimension and resolution in Commutative=20
Algebra |

9:00 - 10:00 | Konstantin Mischaikow |
Invited tutorial: Towards=
=20
an Algebraic Framework for Nonlinear Dynamics |

10:00 - 10:30 | Peter Schuster |
Contributed talk: Eliminati=
ng=20
Krull's Lemma for Horn Clauses |

30min break | ||

11:00 - 12:00 | Ana Romero |
Invited talk: Spectral=20
sequences for computing persistent homology |

12:00 - 12:30 | Philippe Malbos |
Contributed talk: Linear=20
rewriting and homology of associative algebras |

lunch break (1h45) | ||

14:15 - 15:15 | Grant Passmore |
Invited talk: Exact=20
global optimization on demand |

15:15 - 15:45 | Bas Spitters |
Contributed talk: Construct=
ive=20
algebra and geometric mathematics |

15:45 - 16:15 | Bruno Grenet |
Contributed talk: Computing=20
low-degree factors of lacunary polynomials: a Newton-Puiseux=20
approach |

Slides
#### Alain Giorgetti, Richard Genestier and Valerio =
Senni:=20
*Software Engineering and Enumerative Combinatorics*

#### Timothy Gowers: *Fully automatic problem solving =
with=20
human-style output.*

#### Bruno Grenet: *Computing low-degree factors of =
lacunary=20
polynomials: a Newton-Puiseux approach*

#### Alain Herremann: *How to define constructivity? =
Some few=20
things we can learn from history.*

#### Philippe Malbos: *Linear rewriting and homology of =
associative=20
algebras*

We report on the formal verification of an irrationality proof of = the=0A= evaluation at 3 of the Riemann zeta function. This verification uses=0A= the Coq proof assistant in conjunction with algorithmic calculations=0A= in Maple. This irrationality result was first proved by Ap=C3=A9ry = in=0A= 1978, and our formalization follows the proof path of his original=0A= presentation. The crux of it is to establish that some sequences=0A= satisfy a common recurrence. We formally prove this by an a=0A= posteriori verification of calculations performed by a Maple=0A= session. This bases on computer-algebra algorithms implementing=0A= Zeilberger's approach of creative telescoping. This experience=0A= illustrates the limits of the belief that creative telescoping can=0A= discover recurrences for holonomic sequences that are easily checked a=0A= posteriori. We discuss this observation and describe the protocol we=0A= devised in order to produce complete formal proofs of the recurrences.=0A= Beside establishing the recurrences, our proof combines the=0A= formalization of arithmetical ingredients and of some asymptotic=0A= analysis.=0A= =0A= Joint work with Assia Mahboubi, Thomas Sibut-Pinote, and Enrico Tassi.=0A=

We present results on the frontier between two research = domains,=0A= namely enumerative combinatorics and software engineering, and show=0A= how each domain takes profit from the other one.=0A=

I shall describe a program that Mohan Ganesalingam and I created = that=0A= proves simple statements in elementary abstract analysis. I shall also=0A= discuss the broader project of which this is intended to be just a=0A= preliminary step. Briefly, the aim is to write a series of programs=0A= that solve problems in a "fully human" way, meaning that they do not=0A= undertake any search that a human mathematician would not consider=0A= undertaking. At first, this seems to be sacrificing everything that=0A= makes a computer worth using. However, I shall attempt to explain why=0A= we regard this view as mistaken=0A=

I will present a new polynomial-time algorithm for the computation = of=0A= the irreducible factors of degree at most d, with multiplicity, of=0A= multivariate lacunary polynomials over fields of characteristic zero.=0A= The lacunary representation of a polynomial is the list of its nonzero=0A= terms, and the size of this representation is in particular=0A= logarithmic in the degree of the polynomial. Lacunary polynomials can=0A= have factors of exponential size which are therefore not=0A= polynomial-time computable, whence the restriction on the degree of=0A= the factors that are computed.=0A= =0A= The algorithm is a deterministic reduction to the computation of=0A= irreducible factors of degree at most d of univariate lacunary=0A= polynomials on the one hand and to the factorization of low-degree=0A= multivariate polynomials on the other hand. The reduction runs in=0A= time polynomial in the lacunary size of the input polynomial and in=0A= d. As a result, we obtain a new polynomial-time algorithm for the=0A= computation of low-degree factors, with multiplicity, of multivariate=0A= lacunary polynomials over number fields, but our method also gives=0A= partial results for other fields, such as the fields of p-adic numbers=0A= or for absolute or approximate factorization for instance.=0A= =0A= The core of the algorithm uses the Newton polygon of the input=0A= polynomial, and its validity is based on the Newton-Puiseux expansion=0A= of roots of bivariate polynomials. In particular, we bound the=0A= valuation of expressions of expressions of the form f(X,=CF=86) where f = is=0A= a lacunary polynomial and =CF=86 a Puiseux series whose = vanishing=0A= polynomial has low degree.=0A=

Turing (1937) offers to set the idea of calculability in = arithmetic.=0A= Descartes (1637) offers to set the idea of constructibility in=0A= geometry. We will compare the two texts and show how and why they are=0A= similar in many respects.=0A=

Slides
#### Konstantin Mischaikow: *Towards an Algebraic =
Framework for=20
Nonlinear Dynamics*

#### Luca Moci: *Matroids over a ring: motivations, =
examples,=20
applications.*

We introduce the notion of higher dimensional linear rewriting = system=0A= for presentations of algebras generalizing the notion of=0A= noncommutative Gr=C3=B6bner bases. The aim is twofold, 1/ allow = more=0A= possibilities of termination orders than those associated to = Gr=C3=B6bner=0A= bases, only based on monomial orders, 2/ give a description obtained=0A= by rewriting of higher syzygies for presentations of algebras.=0A= =0A= In homological algebra, constructive methods based on noncommutative=0A= Gr=C3=B6bner bases were developed to compute projective resolutions = by=0A= Anick, Green, Berger... In particular, they can be used to study=0A= homological properties of associative algebras such as Koszulness. We=0A= explain how these constructions fit into the general setting of higher=0A= dimensional rewriting theory and how linear rewriting allows more=0A= flexibility for the computation of homological properties of=0A= associative algebras.=0A= =0A= This is a joint work with Yves Guiraud and Eric Hoffbeck.=0A=

The global dynamics of nonlinear systems can exhibit structures = over=0A= wide varieties of temporal and spatial scales and the same phenomenon=0A= is true with respect to parameters. However, from an experimental or=0A= computational perspective only a finite amount of information can be=0A= collected and measurements can only be made up to a certain level of=0A= precision. With this in mind I will argue that we need an alternative=0A= description to the qualitative theory of dynamics, preferably based on=0A= principles that are easily accessed computationally. I will present=0A= some results that represent efforts to develop an algebraic framework=0A= for dynamical systems that is based on tools and techniques from=0A= combinatorics and algebraic topology.=0A=

Slides
#### Anders M=C3=B6rtberg and Cyril Cohen: *Formalizing =
elementary=20
divisor rings in Coq*

#### Grant Passmore: *Exact global optimization on=20
demand*

#### Claude Quitt=C3=A9: *Playing with monomials of =
k[X_1, =E2=80=A6,=20
X_n]*

#### Christophe Raffalli: *Hilbert's 17th problem via=20
cut-elimination*

#### Ana Romero: *Spectral sequences for computing =
persistent=20
homology*

Several objects can be associated to a list of vectors with = integer=0A= coordinates: among others, a family of tori called toric arrangement,=0A= a convex polytope called zonotope, a function called vector partition=0A= function; these objects have been described in a recent book by De=0A= Concini and Procesi. The linear algebra of the list of vectors is=0A= axiomatized by the combinatorial notion of a matroid; but several=0A= properties of the objects above depend also on the arithmetics of the=0A= list. This can be encoded by the notion of a "matroid over=0A= Z". Similarly, applications to tropical geometry suggest the=0A= introduction of matroids over a discrete valuation ring. Motivated by=0A= the examples above, we introduce the more general notion of a "matroid=0A= over a commutative ring R". Such a matroid arises for example from a=0A= list of elements in a R-module. When R is a Dedekind domain, we can=0A= extend the usual properties and operations holding for matroids (e.g.,=0A= duality). We can also compute the Tutte-Grothendieck ring of matroids=0A= over R; the class of a matroid in such a ring specializes to several=0A= invariants, such as the Tutte polynomial and the Tutte=0A= quasipolynomial. We will also outline other possible applications and=0A= open problems.=0A= =0A= (Joint work with Alex Fink).=0A=

An elementary divisor ring is a commutative ring where every matrix = is=0A= equivalent to a matrix in Smith normal form. It is well known that=0A= principal ideal domains are elementary divisor rings, but it is an=0A= open problem whether the generalization to B=C3=A9zout domains, rings = where=0A= every finitely generated ideal is principal, are elementary divisor=0A= rings or not. We have formalized, using the Coq proof assistant=0A= together with the SSReflect extension, different extension that we can=0A= extend B=C3=A9zout domains with in order to show that they are = elementary=0A= divisor rings. The extensions we have considered are: existence of a=0A= gdco operation, adequacy, Krull dimension less than or equal to 1 and=0A= rings where strict divisibility is well-founded.=0A=

Joint work with Leonardo de Moura of Microsoft Research, Redmond.=0A= =0A= We present a method for exact global nonlinear optimization based on a=0A= real algebraic adaptation of the conflict-driven clause learning=0A= (CDCL) approach of modern SAT solving. This method allows polynomial=0A= objective functions to be constrained by real algebraic constraint=0A= systems with arbitrary boolean structure. Moreover, it can correctly=0A= determine when an objective function is unbounded, and can compute=0A= exact infima and suprema when they exist. The method requires=0A= computations over real closed fields containing infinitesimals=0A= (cf. [1]).=0A= =0A= References:=0A= 1. Leonardo de Moura and Grant Olney Passmore. Computation in Real=0A= Closed Infinitesimal and Transcendental Extensions of the Rationals.=0A= In Proceedings of the 24th International Conference on Automated=0A= Deduction (CADE) (2013)=0A=

The context is the graded resolution of monomial ideals of k[X_1, = =E2=80=A6,=0A= X_n], where k is a field. The speaker wishes to explain carefully some=0A= experiments which led him to understand parts of the correspondance=0A= between the monomial world and the simplicial world. In particular :=0A= Stanley-Reisner correspondance, various "fine-grading" syzygies=0A= formulas (Hochster, Bayer-Charalambous-Popescu), Alexander duality,=0A= etc. Tools: algebraic and simplicial Koszul complexes.=0A=

Hilbert's seventeen problem, solved by Artin, says that every = positive=0A= polynomial can be written as a sum of squares of rational=0A= fraction. Since Artin, effective proof have been given by Lombardi -=0A= Roy - Perrucci for the latest one which give a bound to the degree as=0A= a tower of five exponentials.=0A= =0A= We will see how such a proof can be presented as a result of cut=0A= elimination, showing that replacing model theory by proof theory is a=0A= possible method to make a result effective.=0A= =0A= The main contribution of our work is the fact that we implemented the=0A= procedure and we introduced a notion of PBDD that requires smaller=0A= degrees, making it possible to extract the wanted equalities yet only=0A= for the simplest positive polynomials (which was not possible before=0A= from such an effective proof).=0A=

Slides
#### Peter Schuster: *Eliminating Krull's Lemma for =
Horn=20
Clauses*

#### Francis Sergeraert: *Spectral Sequences =
downgraded to=20
elementary Gauss Reductions*

#### Bas Spitters: *Constructive algebra and geometric=20
mathematics*

#### Claire T=C3=AAte: *Depth, dimension and resolution in =
Commutative=20
Algebra*

#### Xavier Caruso, David Roe and Tristan Vaccon: =
*Tracking p-adic=20
precision*

------=_NextPart_000_0000_01D1462F.BD948710
Content-Type: text/css;
charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable
Content-Location: http://perso.crans.org/cohen/map2014/css/default.css
body {
margin: 0px auto; width: 700px; color: black; font-family: verdana; =
font-size: 18px;
}
div#content {
text-align: justify;
}
div#content h1 {
text-align: center;
}
div#content table {
width: 700px;
}
div#content pre {
font-size: 15px;
}
div#header {
padding: 12px 0px; margin-bottom: 30px; border-bottom-color: red; =
border-bottom-width: 2px; border-bottom-style: solid;
}
div#logo a {
color: black; font-size: 18px; font-weight: bold; text-decoration: =
none; float: left;
}
div#header #navigation {
text-align: right;
}
div#header #navigation a {
color: black; text-transform: uppercase; font-size: 16px; font-weight: =
bold; text-decoration: none; margin-left: 12px;
}
div#footer {
padding: 12px 0px; text-align: right; color: rgb(85, 85, 85); =
font-size: 12px; margin-top: 30px; border-top-color: red; =
border-top-width: 2px; border-top-style: solid;
}
h1 {
font-size: 24px;
}
h2 {
font-size: 20px;
}
div.info {
color: rgb(85, 85, 85); font-size: 14px; font-style: italic;
}
.schedule {
border: 2px solid black; border-image: none; border-collapse: collapse;
}
.schedule td {
border: 1px solid black; border-image: none;
}
.time {
width: 160px;
}
.who {
width: 200px; text-align: left;
}
.talk {
width: 440px; text-align: left;
}
.talk a {
text-decoration: none;
}
------=_NextPart_000_0000_01D1462F.BD948710
Content-Type: application/octet-stream
Content-Transfer-Encoding: quoted-printable
Content-Location: http://openfontlibrary.org/face/grundschrift
@font-face {
font-family: GrundschriftBold;
src: =
url(/assets/fonts/grundschrift/34791c82d6efc31c7344cb450c4a2c1c/3349e8178=
4a7d0d0390648bf807b669a/GrundschriftBold.otf) format("opentype");
font-weight: bold;
font-style: normal;
}
@font-face {
font-family: GrundschriftKontur;
src: =
url(/assets/fonts/grundschrift/34791c82d6efc31c7344cb450c4a2c1c/640f409e0=
9f210c6e9696b26cfc3951f/GrundschriftKontur.otf) format("opentype");
font-weight: normal;
font-style: normal;
}
@font-face {
font-family: GrundschriftNormal;
src: =
url(/assets/fonts/grundschrift/34791c82d6efc31c7344cb450c4a2c1c/d3fa37979=
cd87a8e5e7eeec4d386d5aa/GrundschriftNormal.otf) format("opentype");
font-weight: normal;
font-style: normal;
}
@font-face {
font-family: GrundschriftPunkt;
src: =
url(/assets/fonts/grundschrift/34791c82d6efc31c7344cb450c4a2c1c/5084732bd=
96eabfe0bfeb11347c222fd/GrundschriftPunkt.otf) format("opentype");
font-weight: normal;
font-style: normal;
}
@font-face {
font-family: GrundschriftRegular;
src: =
url(/assets/fonts/grundschrift/c118292e03bce13629cacdfbafbb084d/66a2c543f=
aff2aca0eb5774cb9714f25/GrundschriftRegular.otf) format("opentype");
font-weight: normal;
font-style: normal;
}
@font-face {
font-family: Grundschrift;
src: =
url(/assets/fonts/grundschrift/34791c82d6efc31c7344cb450c4a2c1c/3349e8178=
4a7d0d0390648bf807b669a/GrundschriftBold.otf) format("opentype");
font-weight: bold;
font-style: normal;
}
@font-face {
font-family: Grundschrift;
src: =
url(/assets/fonts/grundschrift/34791c82d6efc31c7344cb450c4a2c1c/640f409e0=
9f210c6e9696b26cfc3951f/GrundschriftKontur.otf) format("opentype");
font-weight: normal;
font-style: normal;
}
@font-face {
font-family: Grundschrift;
src: =
url(/assets/fonts/grundschrift/34791c82d6efc31c7344cb450c4a2c1c/d3fa37979=
cd87a8e5e7eeec4d386d5aa/GrundschriftNormal.otf) format("opentype");
font-weight: normal;
font-style: normal;
}
@font-face {
font-family: Grundschrift;
src: =
url(/assets/fonts/grundschrift/34791c82d6efc31c7344cb450c4a2c1c/5084732bd=
96eabfe0bfeb11347c222fd/GrundschriftPunkt.otf) format("opentype");
font-weight: normal;
font-style: normal;
}
@font-face {
font-family: Grundschrift;
src: =
url(/assets/fonts/grundschrift/c118292e03bce13629cacdfbafbb084d/66a2c543f=
aff2aca0eb5774cb9714f25/GrundschriftRegular.otf) format("opentype");
font-weight: normal;
font-style: normal;
}
------=_NextPart_000_0000_01D1462F.BD948710
Content-Type: application/octet-stream
Content-Transfer-Encoding: quoted-printable
Content-Location: http://openfontlibrary.org/face/freeuniversal
@font-face {
font-family: FreeUniversalBold;
src: =
url(/assets/fonts/freeuniversal/5077bdf47767ac210dd15ea83870df66/7952a9d9=
16c9338fb6cbbaa6f70c630c/FreeUniversalBold.ttf) format("truetype");
font-weight: bold;
font-style: normal;
}
@font-face {
font-family: FreeUniversalBoldItalic;
src: =
url(/assets/fonts/freeuniversal/5077bdf47767ac210dd15ea83870df66/e2619057=
037d5bcee341cf86b4bfd55a/FreeUniversalBoldItalic.ttf) =
format("truetype");
font-weight: bold;
font-style: italic;
}
@font-face {
font-family: FreeUniversalItalic;
src: =
url(/assets/fonts/freeuniversal/5077bdf47767ac210dd15ea83870df66/d435b9e2=
7ac6476c1c5d009830de9fdd/FreeUniversalItalic.ttf) format("truetype");
font-weight: normal;
font-style: italic;
}
@font-face {
font-family: FreeUniversalRegular;
src: =
url(/assets/fonts/freeuniversal/5077bdf47767ac210dd15ea83870df66/0ae90cb4=
327d4bce8721841d9bb80a7e/FreeUniversalRegular.ttf) format("truetype");
font-weight: normal;
font-style: normal;
}
@font-face {
font-family: FreeUniversal;
src: =
url(/assets/fonts/freeuniversal/5077bdf47767ac210dd15ea83870df66/7952a9d9=
16c9338fb6cbbaa6f70c630c/FreeUniversalBold.ttf) format("truetype");
font-weight: bold;
font-style: normal;
}
@font-face {
font-family: FreeUniversal;
src: =
url(/assets/fonts/freeuniversal/5077bdf47767ac210dd15ea83870df66/e2619057=
037d5bcee341cf86b4bfd55a/FreeUniversalBoldItalic.ttf) =
format("truetype");
font-weight: bold;
font-style: italic;
}
@font-face {
font-family: FreeUniversal;
src: =
url(/assets/fonts/freeuniversal/5077bdf47767ac210dd15ea83870df66/d435b9e2=
7ac6476c1c5d009830de9fdd/FreeUniversalItalic.ttf) format("truetype");
font-weight: normal;
font-style: italic;
}
@font-face {
font-family: FreeUniversal;
src: =
url(/assets/fonts/freeuniversal/5077bdf47767ac210dd15ea83870df66/0ae90cb4=
327d4bce8721841d9bb80a7e/FreeUniversalRegular.ttf) format("truetype");
font-weight: normal;
font-style: normal;
}
------=_NextPart_000_0000_01D1462F.BD948710--

A filtration of the object to be studied is the heart of both = subjects=0A= persistent homology and spectral sequences; in the talk I will present=0A= the complete relation between them, focusing on constructive and=0A= algorithmic points of views. By using some previous programs for=0A= computing spectral sequences, we obtain persistent homology programs=0A= applicable to spaces not of finite type (provided they are spaces with=0A= effective homology) and with Z-coefficients (significantly=0A= generalizing the usual presentation of persistent homology over a=0A= field).=0A=

Scarpellini [3] has characterised algebraically when in = classical=0A= logic a certain kind of propositional geometric implication in the=0A= language of rings can be proved for commutative rings and for integral=0A= domains, respectively. By interpolation, we extend this=0A= characterisation to the provability of such implications for reduced=0A= rings: that is, commutative rings in which 0 is the only nilpotent=0A= element.=0A= =0A= The characterisation above implies that the theory of integral domains=0A= is conservative for Horn clauses over the theory of reduced rings.=0A= This allows to eliminate Krull's Lemma for commutative rings from some=0A= of the so- called short and elegant proofs in commutative algebra in=0A= which the general case is reduced to the special case by reduction=0A= modulo a generic prime ideal. The method applies, in particular, to=0A= the example studied in [1, 2, 4]: that the non-constant coecients of=0A= an invertible polynomial are all nilpotent.=0A= =0A= 1. Henrik Persson. An application of the constructive spectrum of a=0A= ring. In Type Theory and the Integrated Logic of Programs. Chalmers=0A= University and University of Goeteborg, 1999. PhD thesis.=0A= =0A= 2. Fred Richman. Nontrivial uses of trivial=0A= rings. Proc. Amer. Math. Soc.,103(4):1012-1014, 1988.=0A= =0A= 3. Bruno Scarpellini. On the metamathematics of rings and integral=0A= domains. Trans. Amer. Math. Soc., 138:71-96, 1969.=0A= =0A= 4. Peter Schuster. Induction in algebra: a first case study. In 2012=0A= 27th Annual ACM/IEEE Symposium on Logic in Computer Science, pages=0A= 581-585. IEEE Computer Society Publications, 2012. Proceedings, LICS=0A= 2012, Dubrovnik, Croatia, June 2012. Journal version: Log. Methods=0A= Comput. Sci. (3:20) 9 (2013).=0A=

The standard Spectral Sequences of Algebraic Topology had = been=0A= downgraded 25 years ago by Julio Rubio to the Basic Perturbation=0A= Lemma, an "elementary" result of homological algebra, in fact=0A= relatively complex. The talk is devoted to a reduction of this=0A= "lemma" to elementary Gauss reductions, already known by the=0A= Babylonians, combined with the invertibility of 1-x when |x| < 1.=0A=

Vickers observed that predicative techniques from formal topology = are=0A= often preserved under pullbacks of geometric morphisms. This provides=0A= a clear technical advantage to such constructions. Constructive=0A= algebra, as developed by Coquand and Lombardi provides another=0A= important application.=0A= =0A= I will provide a short overview of some recent such results in=0A= analysis, mostly based on our recent article:=0A= =0A= Bas Spitters, Steven Vickers, and Sander Wolters - Gelfand spectra in=0A= Grothendieck toposes using geometric mathematics, 1310.0705, 2013.=0A= under revision for QPL 2012 post-proceedings in EPTCS.=0A= =0A= http://www.cs.ru.nl/~spitters/geoBS.pdf=0A=

First we introduce two fondamental tools in the theory of depth: = the=0A= Koszul complex and the Cech complex for a finite sequence (a_1,=E2=80=A6 = ,a_n)=0A= in a commutative ring. We give some cohomological properties of these=0A= complexes. By using some basic examples, we try to make explicit the=0A= links between depth, Krull dimension and resolutions. At the end we=0A= illustrate a celebrated Serre theorem characterizing regular rings by=0A= existence of finite projective resolutions: we explain THE resolution=0A= of the ideal of a point of an hypersurface.=0A=