

Plenary speakers
 Carlos D'Andrea, Universitat de Barcelona, Spain.
Title: Elimination Theory in positive characteristic.
Abstract.
Several problems of elimination theory involving arithmetic over the integers (like resultants, the Nullstellensatz, etc) have as an outcome a number which if it is not zero modulo a prime p, implies that
classical results over the complex number (dimension, number of zeroes, etc.) "descend" to the residual field. In this talk we will show some of
these properties, applications, as well as some attempts to understand what happens when these invariants do vanish modulo p.
 Enrique Artal, Universidad de Zaragoza, Spain.
Title: Computational methods in the topology of algebraic varieties.
Abstract.
The topological study of algebraic varieties may involve plenty of computational techniques. In the late 20's, Zariski (and van Kampen) gave a method to compute the fundamental group of the complement of an algebraic curve. Though this method had important theoretical consequences its actual use for the application to curves
of degree not so big needs a lot of computation, which involves both standard techniques in commutative algebra (e.g., Groebner basis) and numerical techniques. Even once these groups are computed, we encounter the problem of getting properties for finite presentations of groups. Alexandertype invariants need to be used combining group theory, commutative algebra and algebraic geometry from the computational point of view. In this talk, we present different ways for the application of these techniques, both as empirical testing and a way of proving theorems.
 Mohamed Barakat, University of Siegen, Germany.
Title: How to implement a category on the computer and why?
Abstract.
What does it mean to program a category? Can one program localisations of categories including the derived category formalism and what is this good for? I will try to answer these questions by showing our applications, how far we got, and where we are heading.
 Lawrence C Paulson, University of Cambridge, England.
Title: The Future of Formalised Mathematics.
Abstract.
Recent years have witnessed tremendous achievements in formalised mathematics, including the completion of the Flyspeck project (a machinechecked proof of the Kepler Conjecture) and the formalisation of the odd order theorem, the central limit theorem and Gödel’s second incompleteness theorem. Formalised mathematics has started to attract the attention of mainstream mathematicians such as Harvey Friedman, Tim Gowers and Tom Hales. Nevertheless, there is much disagreement on the details of formalisms (constructive or classical, typed or typeless), proof languages (linear or structured) and automation (minimal, heuristic or algorithmic). The recent translation of the HOL Light multivariate analysis library to Isabelle highlights some of these differences. The speaker will address these issues, referencing recent developments in the formalisation of real algebraic geometry.
 Andrea Solotar, Universidad de Buenos Aires, Argentina.
Title: Rewriting processes, projective resolutions and ambiguities.
Abstract.
The aim of this talk is to explain our method [1] to construct bimodule resolutions of associative algebras using rewriting processes, and generalizing
Bardzell’s wellknown resolution of monomial algebras. This method leads to concrete computations, providing a useful tool for computing invariants associated
to algebras presented by generators and relations. In this talk I will illustrate how to use it by giving some examples. I will also discuss conditions
on the rewriting system that guarantee that the obtained resolution is minimal.
[1] Chouhy, Sergio; Solotar, Andrea, Projective resolutions of associative algebras and ambiguities. To appear in Journal of Algebra. doi: 10.1016/j.jalgebra.2015.02.019. arXiv: 1406.2300.




